deffunc H1( 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 = 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 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 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 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;
verum
end;
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;
hence
ex b1 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 b1 . s = [0,((Obj F) * (s `2))]
by A4; verum