let S be non empty partial non-empty UAStr ; :: thesis: ( S is Group-like implies ( arity (Den ((In (1,(dom the charact of S))),S)) = 0 & arity (Den ((In (2,(dom the charact of S))),S)) = 1 & arity (Den ((In (3,(dom the charact of S))),S)) = 2 ) )
assume A1: S is Group-like ; :: thesis: ( arity (Den ((In (1,(dom the charact of S))),S)) = 0 & arity (Den ((In (2,(dom the charact of S))),S)) = 1 & arity (Den ((In (3,(dom the charact of S))),S)) = 2 )
then ( 1 is OperSymbol of S & 2 is OperSymbol of S & 3 is OperSymbol of S ) by ThA;
then ( In (1,(dom the charact of S)) = 1 & In (2,(dom the charact of S)) = 2 & In (3,(dom the charact of S)) = 3 ) ;
hence ( arity (Den ((In (1,(dom the charact of S))),S)) = 0 & arity (Den ((In (2,(dom the charact of S))),S)) = 1 & arity (Den ((In (3,(dom the charact of S))),S)) = 2 ) by A1, PUA2MSS1:def 1; :: thesis: verum