deffunc H1( 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 = 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
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 ;
per cases ( a in [:{1},(1 -tuples_on the carrier of C1):] or a in [:{2},(3 -tuples_on the carrier of C1):] ) by ;
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 ;
( <*a1*> . 1 = a1 & 1 in {1} ) by ;
then p . 1 = (Obj F) . a1 by ;
then p = <*((Obj F) . a1)*> by ;
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 ;
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 ;
hence x in the carrier' of (CatSign the carrier of C2) by A16, A18, A26, A22; :: thesis: verum
end;
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 ;
then A31: p . 1 = (Obj F) . a1 by ;
( <*a1,a2,a3*> . 3 = a3 & 3 in {1,2,3} ) by ;
then A32: p . 3 = (Obj F) . a3 by ;
( <*a1,a2,a3*> . 2 = a2 & 2 in {1,2,3} ) by ;
then A33: p . 2 = (Obj F) . a2 by ;
len p = 3 by ;
then p = <*((Obj F) . a1),((Obj F) . a2),((Obj F) . a3)*> by ;
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 ;
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 ;
hence x in the carrier' of (CatSign the carrier of C2) by A16, A18, A35, A29; :: thesis: verum
end;
end;
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 o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1),((Obj F) * (o `2))] by A16; :: thesis: verum