let A be non empty set ; :: thesis: for o being OperSymbol of (CatSign A) st ( o `1 = 1 or len (o `2) = 1 ) holds

ex a being Element of A st o = idsym a

let o be OperSymbol of (CatSign A); :: thesis: ( ( o `1 = 1 or len (o `2) = 1 ) implies ex a being Element of A st o = idsym a )

assume A1: ( o `1 = 1 or len (o `2) = 1 ) ; :: thesis: ex a being Element of A st o = idsym a

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 & o = [(o `1),(o `2)] ) or ( o `1 in {2} & o `2 in 3 -tuples_on A ) ) by MCART_1:10, MCART_1:21;

then consider a being set such that

A3: a in A and

A4: o `2 = <*a*> by A1, CARD_1:def 7, FINSEQ_2:135, TARSKI:def 1;

reconsider a = a as Element of A by A3;

take a ; :: thesis: o = idsym a

thus o = idsym a by A1, A2, A4, CARD_1:def 7, TARSKI:def 1; :: thesis: verum

ex a being Element of A st o = idsym a

let o be OperSymbol of (CatSign A); :: thesis: ( ( o `1 = 1 or len (o `2) = 1 ) implies ex a being Element of A st o = idsym a )

assume A1: ( o `1 = 1 or len (o `2) = 1 ) ; :: thesis: ex a being Element of A st o = idsym a

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 & o = [(o `1),(o `2)] ) or ( o `1 in {2} & o `2 in 3 -tuples_on A ) ) by MCART_1:10, MCART_1:21;

then consider a being set such that

A3: a in A and

A4: o `2 = <*a*> by A1, CARD_1:def 7, FINSEQ_2:135, TARSKI:def 1;

reconsider a = a as Element of A by A3;

take a ; :: thesis: o = idsym a

thus o = idsym a by A1, A2, A4, CARD_1:def 7, TARSKI:def 1; :: thesis: verum