let X be non empty set ; :: thesis: for f1, f2, f3 being non empty homogeneous PartFunc of (X *),X st arity f1 = 0 & arity f2 = 1 & arity f3 = 2 holds
for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> c= the charact of S holds
S is Group-like
let f1, f2, f3 be non empty homogeneous PartFunc of (X *),X; :: thesis: ( arity f1 = 0 & arity f2 = 1 & arity f3 = 2 implies for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> c= the charact of S holds
S is Group-like )
assume 01: arity f1 = 0 ; :: thesis: ( not arity f2 = 1 or not arity f3 = 2 or for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> c= the charact of S holds
S is Group-like )
assume 02: arity f2 = 1 ; :: thesis: ( not arity f3 = 2 or for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> c= the charact of S holds
S is Group-like )
assume 03: arity f3 = 2 ; :: thesis: for S being non empty UAStr st the carrier of S = X & <*f1,f2,f3*> c= the charact of S holds
S is Group-like
let S be non empty UAStr ; :: thesis: ( the carrier of S = X & <*f1,f2,f3*> c= the charact of S implies S is Group-like )
assume 04: ( the carrier of S = X & <*f1,f2,f3*> c= the charact of S ) ; :: thesis: S is Group-like
05: dom <*f1,f2,f3*> = Seg 3 by FINSEQ_2:124;
hence Seg 3 c= dom the charact of S by 04, RELAT_1:11; :: according to ABSRED_0:def 29 :: thesis: for f being non empty homogeneous PartFunc of ( the carrier of S *), the carrier of S holds
( ( f = the charact of S . 1 implies arity f = 0 ) & ( f = the charact of S . 2 implies arity f = 1 ) & ( f = the charact of S . 3 implies arity f = 2 ) )
let f be non empty homogeneous PartFunc of ( the carrier of S *), the carrier of S; :: thesis: ( ( f = the charact of S . 1 implies arity f = 0 ) & ( f = the charact of S . 2 implies arity f = 1 ) & ( f = the charact of S . 3 implies arity f = 2 ) )
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_3:1, ENUMSET1:def 1;
then ( the charact of S . 1 = <*f1,f2,f3*> . 1 & the charact of S . 2 = <*f1,f2,f3*> . 2 & the charact of S . 3 = <*f1,f2,f3*> . 3 ) by 04, 05, GRFUNC_1:2;
hence ( ( f = the charact of S . 1 implies arity f = 0 ) & ( f = the charact of S . 2 implies arity f = 1 ) & ( f = the charact of S . 3 implies arity f = 2 ) ) by 01, 02, 03, FINSEQ_1:45; :: thesis: verum