deffunc H1( SortSymbol of (CatSign the carrier of C1)) -> set = [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
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 A5:
(
a in dom Up &
x = Up . a )
by FUNCT_1:def 5;
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 Def5;
then
(
a `2 in 2
-tuples_on the
carrier of
C1 &
a = [(a `1 ),(a `2 )] )
by MCART_1:12, MCART_1:23;
then consider a1,
a2 being
set such that A6:
(
a1 in the
carrier of
C1 &
a2 in the
carrier of
C1 &
a `2 = <*a1,a2*> )
by Th10;
reconsider a1 =
a1,
a2 =
a2 as
Object of
C1 by A6;
(
rng <*a1,a2*> c= the
carrier of
C1 &
dom (Obj F) = the
carrier of
C1 )
by FUNCT_2:def 1;
then A7:
dom ((Obj F) * <*a1,a2*>) =
dom <*a1,a2*>
by RELAT_1:46
.=
Seg 2
by FINSEQ_3:29
;
then reconsider p =
(Obj F) * <*a1,a2*> as
FinSequence by FINSEQ_1:def 2;
(
<*a1,a2*> . 1
= a1 &
<*a1,a2*> . 2
= a2 & 1
in {1,2} & 2
in {1,2} )
by FINSEQ_1:61, TARSKI:def 2;
then
(
len p = 2 &
p . 1
= (Obj F) . a1 &
p . 2
= (Obj F) . a2 )
by A7, FINSEQ_1:4, FINSEQ_1:def 3, FUNCT_1:22;
then
p = <*((Obj F) . a1),((Obj F) . a2)*>
by FINSEQ_1:61;
then
p is
Element of 2
-tuples_on the
carrier of
C2
by FINSEQ_2:121;
then
( the
carrier of
(CatSign the carrier of C2) = [:{0 },(2 -tuples_on the carrier of C2):] &
p in 2
-tuples_on the
carrier of
C2 )
by Def5;
then
[0 ,p] in the
carrier of
(CatSign the carrier of C2)
by ZFMISC_1:128;
hence
x in the
carrier of
(CatSign the carrier of C2)
by A4, A5, A6;
:: thesis: 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: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 s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0 ,((Obj F) * (s `2 ))]
by A4; :: thesis: verum