deffunc H_{1}( OperSymbol of (CatSign the carrier of C1)) -> object = [($1 `1),((Obj F) * ($1 `2))];

consider Up being Function such that

A15: dom Up = the carrier' of (CatSign the carrier of C1) and

A16: for s being OperSymbol 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 o being OperSymbol of (CatSign the carrier of C1) holds b_{1} . o = [(o `1),((Obj F) * (o `2))]
by A16; :: thesis: verum

consider Up being Function such that

A15: dom Up = the carrier' of (CatSign the carrier of C1) and

A16: for s being OperSymbol 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 A15, 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

A17: a in dom Up and

A18: x = Up . a by FUNCT_1:def 3;

A19: the carrier' of (CatSign the carrier of C1) = [:{1},(1 -tuples_on the carrier of C1):] \/ [:{2},(3 -tuples_on the carrier of C1):] by Def3;

reconsider a = a as OperSymbol of (CatSign the carrier of C1) by A15, A17;

end;assume x in rng Up ; :: thesis: x in the carrier' of (CatSign the carrier of C2)

then consider a being object such that

A17: a in dom Up and

A18: x = Up . a by FUNCT_1:def 3;

A19: the carrier' of (CatSign the carrier of C1) = [:{1},(1 -tuples_on the carrier of C1):] \/ [:{2},(3 -tuples_on the carrier of C1):] by Def3;

reconsider a = a as OperSymbol of (CatSign the carrier of C1) by A15, A17;

per cases
( a in [:{1},(1 -tuples_on the carrier of C1):] or a in [:{2},(3 -tuples_on the carrier of C1):] )
by A19, XBOOLE_0:def 3;

end;

suppose A20:
a in [:{1},(1 -tuples_on the carrier of C1):]
; :: thesis: x in the carrier' of (CatSign the carrier of C2)

then
a `2 in 1 -tuples_on the carrier of C1
by MCART_1:12;

then consider a1 being set such that

A21: a1 in the carrier of C1 and

A22: a `2 = <*a1*> by FINSEQ_2:135;

reconsider a1 = a1 as Object of C1 by A21;

( rng <*a1*> c= the carrier of C1 & dom (Obj F) = the carrier of C1 ) by FUNCT_2:def 1;

then A23: dom ((Obj F) * <*a1*>) = dom <*a1*> by RELAT_1:27

.= Seg 1 by FINSEQ_1:38 ;

then reconsider p = (Obj F) * <*a1*> as FinSequence by FINSEQ_1:def 2;

A24: len p = 1 by A23, FINSEQ_1:def 3;

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

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

then p = <*((Obj F) . a1)*> by A24, FINSEQ_1:40;

then p is Element of 1 -tuples_on the carrier of C2 by FINSEQ_2:98;

then A25: [1,p] in [:{1},(1 -tuples_on the carrier of C2):] by ZFMISC_1:105;

A26: a `1 = 1 by A20, MCART_1:12;

the carrier' of (CatSign the carrier of C2) = [:{1},(1 -tuples_on the carrier of C2):] \/ [:{2},(3 -tuples_on the carrier of C2):] by Def3;

then [1,p] in the carrier' of (CatSign the carrier of C2) by A25, XBOOLE_0:def 3;

hence x in the carrier' of (CatSign the carrier of C2) by A16, A18, A26, A22; :: thesis: verum

end;then consider a1 being set such that

A21: a1 in the carrier of C1 and

A22: a `2 = <*a1*> by FINSEQ_2:135;

reconsider a1 = a1 as Object of C1 by A21;

( rng <*a1*> c= the carrier of C1 & dom (Obj F) = the carrier of C1 ) by FUNCT_2:def 1;

then A23: dom ((Obj F) * <*a1*>) = dom <*a1*> by RELAT_1:27

.= Seg 1 by FINSEQ_1:38 ;

then reconsider p = (Obj F) * <*a1*> as FinSequence by FINSEQ_1:def 2;

A24: len p = 1 by A23, FINSEQ_1:def 3;

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

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

then p = <*((Obj F) . a1)*> by A24, FINSEQ_1:40;

then p is Element of 1 -tuples_on the carrier of C2 by FINSEQ_2:98;

then A25: [1,p] in [:{1},(1 -tuples_on the carrier of C2):] by ZFMISC_1:105;

A26: a `1 = 1 by A20, MCART_1:12;

the carrier' of (CatSign the carrier of C2) = [:{1},(1 -tuples_on the carrier of C2):] \/ [:{2},(3 -tuples_on the carrier of C2):] by Def3;

then [1,p] in the carrier' of (CatSign the carrier of C2) by A25, XBOOLE_0:def 3;

hence x in the carrier' of (CatSign the carrier of C2) by A16, A18, A26, A22; :: thesis: verum

suppose A27:
a in [:{2},(3 -tuples_on the carrier of C1):]
; :: thesis: x in the carrier' of (CatSign the carrier of C2)

then
a `2 in 3 -tuples_on the carrier of C1
by MCART_1:12;

then consider a1, a2, a3 being object such that

A28: ( a1 in the carrier of C1 & a2 in the carrier of C1 & a3 in the carrier of C1 ) and

A29: a `2 = <*a1,a2,a3*> by FINSEQ_2:139;

reconsider a1 = a1, a2 = a2, a3 = a3 as Object of C1 by A28;

( rng <*a1,a2,a3*> c= the carrier of C1 & dom (Obj F) = the carrier of C1 ) by FUNCT_2:def 1;

then A30: dom ((Obj F) * <*a1,a2,a3*>) = dom <*a1,a2,a3*> by RELAT_1:27

.= Seg 3 by FINSEQ_1:89 ;

then reconsider p = (Obj F) * <*a1,a2,a3*> as FinSequence by FINSEQ_1:def 2;

( <*a1,a2,a3*> . 1 = a1 & 1 in {1,2,3} ) by ENUMSET1:def 1, FINSEQ_1:45;

then A31: p . 1 = (Obj F) . a1 by A30, FINSEQ_3:1, FUNCT_1:12;

( <*a1,a2,a3*> . 3 = a3 & 3 in {1,2,3} ) by ENUMSET1:def 1, FINSEQ_1:45;

then A32: p . 3 = (Obj F) . a3 by A30, FINSEQ_3:1, FUNCT_1:12;

( <*a1,a2,a3*> . 2 = a2 & 2 in {1,2,3} ) by ENUMSET1:def 1, FINSEQ_1:45;

then A33: p . 2 = (Obj F) . a2 by A30, FINSEQ_3:1, FUNCT_1:12;

len p = 3 by A30, FINSEQ_1:def 3;

then p = <*((Obj F) . a1),((Obj F) . a2),((Obj F) . a3)*> by A31, A33, A32, FINSEQ_1:45;

then p is Element of 3 -tuples_on the carrier of C2 by FINSEQ_2:104;

then A34: [2,p] in [:{2},(3 -tuples_on the carrier of C2):] by ZFMISC_1:105;

A35: a `1 = 2 by A27, MCART_1:12;

the carrier' of (CatSign the carrier of C2) = [:{1},(1 -tuples_on the carrier of C2):] \/ [:{2},(3 -tuples_on the carrier of C2):] by Def3;

then [2,p] in the carrier' of (CatSign the carrier of C2) by A34, XBOOLE_0:def 3;

hence x in the carrier' of (CatSign the carrier of C2) by A16, A18, A35, A29; :: thesis: verum

end;then consider a1, a2, a3 being object such that

A28: ( a1 in the carrier of C1 & a2 in the carrier of C1 & a3 in the carrier of C1 ) and

A29: a `2 = <*a1,a2,a3*> by FINSEQ_2:139;

reconsider a1 = a1, a2 = a2, a3 = a3 as Object of C1 by A28;

( rng <*a1,a2,a3*> c= the carrier of C1 & dom (Obj F) = the carrier of C1 ) by FUNCT_2:def 1;

then A30: dom ((Obj F) * <*a1,a2,a3*>) = dom <*a1,a2,a3*> by RELAT_1:27

.= Seg 3 by FINSEQ_1:89 ;

then reconsider p = (Obj F) * <*a1,a2,a3*> as FinSequence by FINSEQ_1:def 2;

( <*a1,a2,a3*> . 1 = a1 & 1 in {1,2,3} ) by ENUMSET1:def 1, FINSEQ_1:45;

then A31: p . 1 = (Obj F) . a1 by A30, FINSEQ_3:1, FUNCT_1:12;

( <*a1,a2,a3*> . 3 = a3 & 3 in {1,2,3} ) by ENUMSET1:def 1, FINSEQ_1:45;

then A32: p . 3 = (Obj F) . a3 by A30, FINSEQ_3:1, FUNCT_1:12;

( <*a1,a2,a3*> . 2 = a2 & 2 in {1,2,3} ) by ENUMSET1:def 1, FINSEQ_1:45;

then A33: p . 2 = (Obj F) . a2 by A30, FINSEQ_3:1, FUNCT_1:12;

len p = 3 by A30, FINSEQ_1:def 3;

then p = <*((Obj F) . a1),((Obj F) . a2),((Obj F) . a3)*> by A31, A33, A32, FINSEQ_1:45;

then p is Element of 3 -tuples_on the carrier of C2 by FINSEQ_2:104;

then A34: [2,p] in [:{2},(3 -tuples_on the carrier of C2):] by ZFMISC_1:105;

A35: a `1 = 2 by A27, MCART_1:12;

the carrier' of (CatSign the carrier of C2) = [:{1},(1 -tuples_on the carrier of C2):] \/ [:{2},(3 -tuples_on the carrier of C2):] by Def3;

then [2,p] in the carrier' of (CatSign the carrier of C2) by A34, XBOOLE_0:def 3;

hence x in the carrier' of (CatSign the carrier of C2) by A16, A18, A35, A29; :: thesis: verum

hence ex b

for o being OperSymbol of (CatSign the carrier of C1) holds b