let A be non empty set ; :: thesis: for o being OperSymbol of () st ( o `1 = 2 or len (o `2) = 3 ) holds
ex a, b, c being Element of A st o = compsym (a,b,c)

let o be OperSymbol of (); :: thesis: ( ( o `1 = 2 or len (o `2) = 3 ) implies ex a, b, c being Element of A st o = compsym (a,b,c) )
assume A1: ( o `1 = 2 or len (o `2) = 3 ) ; :: thesis: ex a, b, c being Element of A st o = compsym (a,b,c)
the carrier' of () = [:{1},():] \/ [:{2},():] by Def3;
then ( o in [:{1},():] or o in [:{2},():] ) by XBOOLE_0:def 3;
then A2: ( ( o `1 in {1} & o `2 in 1 -tuples_on A ) or ( o `1 in {2} & o `2 in 3 -tuples_on A & o = [(o `1),(o `2)] ) ) by ;
then consider a, b, c being object such that
A3: ( a in A & b in A & c in A ) and
A4: o `2 = <*a,b,c*> by ;
reconsider a = a, b = b, c = c as Element of A by A3;
take a ; :: thesis: ex b, c being Element of A st o = compsym (a,b,c)
take b ; :: thesis: ex c being Element of A st o = compsym (a,b,c)
take c ; :: thesis: o = compsym (a,b,c)
thus o = compsym (a,b,c) by ; :: thesis: verum