let A be non empty set ; for o being OperSymbol of (CatSign A) 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 (CatSign A); ( ( 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 )
; ex a, b, c being Element of A st o = compsym (a,b,c)
the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]
by Def3;
then
( o in [:{1},(1 -tuples_on A):] or o in [:{2},(3 -tuples_on A):] )
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 MCART_1:10, MCART_1:21;
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 A1, CARD_1:def 7, FINSEQ_2:139, TARSKI:def 1;
reconsider a = a, b = b, c = c as Element of A by A3;
take
a
; ex b, c being Element of A st o = compsym (a,b,c)
take
b
; ex c being Element of A st o = compsym (a,b,c)
take
c
; o = compsym (a,b,c)
thus
o = compsym (a,b,c)
by A1, A2, A4, CARD_1:def 7, TARSKI:def 1; verum