deffunc H_{1}( 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 = H_{1}(s)
from FUNCT_1:sch 4();

rng Up c= the carrier of (CatSign the carrier of C2)

hence ex b_{1} 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 b_{1} . s = [0,((Obj F) * (s `2))]
by A4; :: thesis: verum

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 = H

rng Up c= the carrier of (CatSign the carrier of C2)

proof

then
Up is Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2)
by A3, FUNCT_2:def 1, RELSET_1:4;
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) = [:{0},(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 FINSEQ_1:44, TARSKI:def 2;

then A10: p . 1 = (Obj F) . a1 by A9, FINSEQ_1:2, FUNCT_1:12;

A11: the carrier of (CatSign the carrier of C2) = [:{0},(2 -tuples_on the carrier of C2):] by Def3;

( <*a1,a2*> . 2 = a2 & 2 in {1,2} ) by FINSEQ_1:44, TARSKI:def 2;

then A12: p . 2 = (Obj F) . a2 by A9, FINSEQ_1:2, FUNCT_1:12;

len p = 2 by A9, FINSEQ_1:def 3;

then p = <*((Obj F) . a1),((Obj F) . a2)*> by A10, A12, FINSEQ_1:44;

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 A11, ZFMISC_1:105;

hence x in the carrier of (CatSign the carrier of C2) by A4, A6, A8; :: thesis: verum

end;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) = [:{0},(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 FINSEQ_1:44, TARSKI:def 2;

then A10: p . 1 = (Obj F) . a1 by A9, FINSEQ_1:2, FUNCT_1:12;

A11: the carrier of (CatSign the carrier of C2) = [:{0},(2 -tuples_on the carrier of C2):] by Def3;

( <*a1,a2*> . 2 = a2 & 2 in {1,2} ) by FINSEQ_1:44, TARSKI:def 2;

then A12: p . 2 = (Obj F) . a2 by A9, FINSEQ_1:2, FUNCT_1:12;

len p = 2 by A9, FINSEQ_1:def 3;

then p = <*((Obj F) . a1),((Obj F) . a2)*> by A10, A12, FINSEQ_1:44;

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 A11, ZFMISC_1:105;

hence x in the carrier of (CatSign the carrier of C2) by A4, A6, A8; :: thesis: verum

hence ex b

for s being SortSymbol of (CatSign the carrier of C1) holds b