let A be non empty set ; :: thesis: for o being OperSymbol of (CatSign A) holds
( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) )
let o be OperSymbol of (CatSign A); :: thesis: ( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) )
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 ( ( o `1 in {1} & o `2 in 1 -tuples_on A ) or ( o `1 in {2} & o `2 in 3 -tuples_on A ) ) by MCART_1:10;
hence ( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) ) by CARD_1:def 7, TARSKI:def 1; :: thesis: verum