let A be set ; :: thesis: for x being object st x in proj2 ( the carrier of (CatSign A) \/ the carrier' of (CatSign A)) holds
x is Function
let x be object ; :: thesis: ( x in proj2 ( the carrier of (CatSign A) \/ the carrier' of (CatSign A)) implies x is Function )
set C1 = the carrier of (CatSign A);
set C2 = the carrier' of (CatSign A);
A1: the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;
A2: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3;
assume x in proj2 ( the carrier of (CatSign A) \/ the carrier' of (CatSign A)) ; :: thesis: x is Function
then x in (proj2 the carrier of (CatSign A)) \/ (proj2 the carrier' of (CatSign A)) by XTUPLE_0:27;

per cases then ( x in proj2 the carrier of (CatSign A) or x in proj2 the carrier' of (CatSign A) ) by XBOOLE_0:def 3;

suppose x in proj2 the carrier of (CatSign A) ; :: thesis: x is Function

then x in 2 -tuples_on A by A1, FUNCT_5:9;
hence x is Function ; :: thesis: verum

end;

suppose x in proj2 the carrier' of (CatSign A) ; :: thesis: x is Function

then x in (proj2 [:{1},(1 -tuples_on A):]) \/ (proj2 [:{2},(3 -tuples_on A):]) by A2, XTUPLE_0:27;

per cases then ( x in proj2 [:{1},(1 -tuples_on A):] or x in proj2 [:{2},(3 -tuples_on A):] ) by XBOOLE_0:def 3;

suppose x in proj2 [:{1},(1 -tuples_on A):] ; :: thesis: x is Function

then x in 1 -tuples_on A by FUNCT_5:9;
hence x is Function ; :: thesis: verum

end;

suppose x in proj2 [:{2},(3 -tuples_on A):] ; :: thesis: x is Function

then x in 3 -tuples_on A by FUNCT_5:9;
hence x is Function ; :: thesis: verum

end;

end;

end;

end;