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 FUNCT_1:sch 4();
rng Up c= the carrier' of (CatSign the carrier of C2)
proof
let x be
object ;
TARSKI:def 3 ( not x in rng Up or x in the carrier' of (CatSign the carrier of C2) )
assume
x in rng Up
;
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;
suppose A20:
a in [:{1},(1 -tuples_on the carrier of C1):]
;
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 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;
verum end; suppose A27:
a in [:{2},(3 -tuples_on the carrier of C1):]
;
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;
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;
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;
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;
verum end;
end;
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;
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; verum