deffunc H1( SortSymbol of (CatSign the carrier of C1)) -> object = [0,((Obj F) * (\$1 `2))];
consider Up being Function such that
A3: dom Up = the carrier of (CatSign the carrier of C1) and
A4: for s being SortSymbol of (CatSign the carrier of C1) holds Up . s = H1(s) from rng Up c= the carrier of (CatSign the carrier of C2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng Up or x in the carrier of (CatSign the carrier of C2) )
assume x in rng Up ; :: thesis: x in the carrier of (CatSign the carrier of C2)
then consider a being object such that
A5: a in dom Up and
A6: x = Up . a by FUNCT_1:def 3;
reconsider a = a as SortSymbol of (CatSign the carrier of C1) by A3, A5;
the carrier of (CatSign the carrier of C1) = [:,(2 -tuples_on the carrier of C1):] by Def3;
then a `2 in 2 -tuples_on the carrier of C1 by MCART_1:12;
then consider a1, a2 being object such that
A7: ( a1 in the carrier of C1 & a2 in the carrier of C1 ) and
A8: a `2 = <*a1,a2*> by FINSEQ_2:137;
reconsider a1 = a1, a2 = a2 as Object of C1 by A7;
( rng <*a1,a2*> c= the carrier of C1 & dom (Obj F) = the carrier of C1 ) by FUNCT_2:def 1;
then A9: dom ((Obj F) * <*a1,a2*>) = dom <*a1,a2*> by RELAT_1:27
.= Seg 2 by FINSEQ_1:89 ;
then reconsider p = (Obj F) * <*a1,a2*> as FinSequence by FINSEQ_1:def 2;
( <*a1,a2*> . 1 = a1 & 1 in {1,2} ) by ;
then A10: p . 1 = (Obj F) . a1 by ;
A11: the carrier of (CatSign the carrier of C2) = [:,(2 -tuples_on the carrier of C2):] by Def3;
( <*a1,a2*> . 2 = a2 & 2 in {1,2} ) by ;
then A12: p . 2 = (Obj F) . a2 by ;
len p = 2 by ;
then p = <*((Obj F) . a1),((Obj F) . a2)*> by ;
then p in 2 -tuples_on the carrier of C2 by FINSEQ_2:101;
then [0,p] in the carrier of (CatSign the carrier of C2) by ;
hence x in the carrier of (CatSign the carrier of C2) by A4, A6, A8; :: thesis: verum
end;
then Up is Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) by ;
hence ex b1 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st
for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0,((Obj F) * (s `2))] by A4; :: thesis: verum