deffunc H1( OperSymbol of (CatSign the carrier of C1)) -> set = [($1 `1 ),((Obj F) * ($1 `2 ))];
consider Up being Function such that
A10:
dom Up = the carrier' of (CatSign the carrier of C1)
and
A11:
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
set ;
:: 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
set such that A12:
(
a in dom Up &
x = Up . a )
by FUNCT_1:def 5;
reconsider a =
a as
OperSymbol of
(CatSign the carrier of C1) by A10, A12;
A13:
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 Def5;
per cases
( a in [:{1},(1 -tuples_on the carrier of C1):] or a in [:{2},(3 -tuples_on the carrier of C1):] )
by A13, XBOOLE_0:def 3;
suppose
a in [:{1},(1 -tuples_on the carrier of C1):]
;
:: thesis: x in the carrier' of (CatSign the carrier of C2)then A14:
(
a `1 = 1 &
a `2 in 1
-tuples_on the
carrier of
C1 &
a = [(a `1 ),(a `2 )] )
by MCART_1:12, MCART_1:23;
then consider a1 being
set such that A15:
(
a1 in the
carrier of
C1 &
a `2 = <*a1*> )
by Th8;
reconsider a1 =
a1 as
Object of
C1 by A15;
(
rng <*a1*> c= the
carrier of
C1 &
dom (Obj F) = the
carrier of
C1 )
by FUNCT_2:def 1;
then A16:
dom ((Obj F) * <*a1*>) =
dom <*a1*>
by RELAT_1:46
.=
Seg 1
by FINSEQ_1:55
;
then reconsider p =
(Obj F) * <*a1*> as
FinSequence by FINSEQ_1:def 2;
(
<*a1*> . 1
= a1 & 1
in {1} )
by FINSEQ_1:57, TARSKI:def 1;
then
(
len p = 1 &
p . 1
= (Obj F) . a1 )
by A16, FINSEQ_1:4, FINSEQ_1:def 3, FUNCT_1:22;
then
p = <*((Obj F) . a1)*>
by FINSEQ_1:57;
then
p is
Element of 1
-tuples_on the
carrier of
C2
by FINSEQ_2:118;
then
( the
carrier' of
(CatSign the carrier of C2) = [:{1},(1 -tuples_on the carrier of C2):] \/ [:{2},(3 -tuples_on the carrier of C2):] &
[1,p] in [:{1},(1 -tuples_on the carrier of C2):] )
by Def5, ZFMISC_1:128;
then
[1,p] in the
carrier' of
(CatSign the carrier of C2)
by XBOOLE_0:def 3;
hence
x in the
carrier' of
(CatSign the carrier of C2)
by A11, A12, A14, A15;
:: thesis: verum end; suppose
a in [:{2},(3 -tuples_on the carrier of C1):]
;
:: thesis: x in the carrier' of (CatSign the carrier of C2)then A17:
(
a `1 = 2 &
a `2 in 3
-tuples_on the
carrier of
C1 &
a = [(a `1 ),(a `2 )] )
by MCART_1:12, MCART_1:23;
then consider a1,
a2,
a3 being
set such that A18:
(
a1 in the
carrier of
C1 &
a2 in the
carrier of
C1 &
a3 in the
carrier of
C1 &
a `2 = <*a1,a2,a3*> )
by Th12;
reconsider a1 =
a1,
a2 =
a2,
a3 =
a3 as
Object of
C1 by A18;
(
rng <*a1,a2,a3*> c= the
carrier of
C1 &
dom (Obj F) = the
carrier of
C1 )
by FUNCT_2:def 1;
then A19:
dom ((Obj F) * <*a1,a2,a3*>) =
dom <*a1,a2,a3*>
by RELAT_1:46
.=
Seg 3
by FINSEQ_3:30
;
then reconsider p =
(Obj F) * <*a1,a2,a3*> as
FinSequence by FINSEQ_1:def 2;
(
<*a1,a2,a3*> . 1
= a1 &
<*a1,a2,a3*> . 2
= a2 &
<*a1,a2,a3*> . 3
= a3 & 1
in {1,2,3} & 2
in {1,2,3} & 3
in {1,2,3} )
by ENUMSET1:def 1, FINSEQ_1:62;
then
(
len p = 3 &
p . 1
= (Obj F) . a1 &
p . 2
= (Obj F) . a2 &
p . 3
= (Obj F) . a3 )
by A19, FINSEQ_1:def 3, FINSEQ_3:1, FUNCT_1:22;
then
p = <*((Obj F) . a1),((Obj F) . a2),((Obj F) . a3)*>
by FINSEQ_1:62;
then
p is
Element of 3
-tuples_on the
carrier of
C2
by FINSEQ_2:124;
then
( the
carrier' of
(CatSign the carrier of C2) = [:{1},(1 -tuples_on the carrier of C2):] \/ [:{2},(3 -tuples_on the carrier of C2):] &
[2,p] in [:{2},(3 -tuples_on the carrier of C2):] )
by Def5, ZFMISC_1:128;
then
[2,p] in the
carrier' of
(CatSign the carrier of C2)
by XBOOLE_0:def 3;
hence
x in the
carrier' of
(CatSign the carrier of C2)
by A11, A12, A17, A18;
:: thesis: 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 A10, FUNCT_2:def 1, RELSET_1:11;
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 A11; :: thesis: verum