let S be non empty non-empty UAStr ; :: thesis: ( S is Group-like implies ( 1 is OperSymbol of S & 2 is OperSymbol of S & 3 is OperSymbol of S ) )
assume A0: Seg 3 c= dom the charact of S ; :: according to ABSRED_0:def 29 :: thesis: ( ex f being non empty homogeneous PartFunc of ( the carrier of S *), the carrier of S st
( ( f = the charact of S . 1 implies arity f = 0 ) & ( f = the charact of S . 2 implies arity f = 1 ) implies ( f = the charact of S . 3 & not arity f = 2 ) ) or ( 1 is OperSymbol of S & 2 is OperSymbol of S & 3 is OperSymbol of S ) )
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_3:1, ENUMSET1:def 1;
hence ( ex f being non empty homogeneous PartFunc of ( the carrier of S *), the carrier of S st
( ( f = the charact of S . 1 implies arity f = 0 ) & ( f = the charact of S . 2 implies arity f = 1 ) implies ( f = the charact of S . 3 & not arity f = 2 ) ) or ( 1 is OperSymbol of S & 2 is OperSymbol of S & 3 is OperSymbol of S ) ) by A0; :: thesis: verum