let X, Y be RealNormSpace; for z being Point of [:X,Y:] holds
( reproj1 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) & reproj2 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) )
let z be Point of [:X,Y:]; ( reproj1 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) & reproj2 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) )
set i1 = In (1,(dom <*X,Y*>));
set i2 = In (2,(dom <*X,Y*>));
D1: dom <*X,Y*> =
Seg (len <*X,Y*>)
by FINSEQ_1:def 3
.=
Seg 2
by FINSEQ_1:44
;
then
1 in dom <*X,Y*>
;
then AS1:
In (1,(dom <*X,Y*>)) = 1
by SUBSET_1:def 8;
2 in dom <*X,Y*>
by D1;
then AS2:
In (2,(dom <*X,Y*>)) = 2
by SUBSET_1:def 8;
set I = (IsoCPNrSP (X,Y)) " ;
set J = IsoCPNrSP (X,Y);
set f1 = reproj1 z;
<*X,Y*> . (In (1,(dom <*X,Y*>))) = X
by AS1, FINSEQ_1:44;
then reconsider R = reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z)) as Function of X,(product <*X,Y*>) ;
reconsider g1 = ((IsoCPNrSP (X,Y)) ") * R as Function of X,[:X,Y:] ;
consider x being Point of X, y being Point of Y such that
P1:
z = [x,y]
by PRVECT_3:18;
P3:
z `2 = y
by P1;
P4: (IsoCPNrSP (X,Y)) . z =
(IsoCPNrSP (X,Y)) . (x,y)
by P1
.=
<*x,y*>
by defISO
;
now for r being Element of X holds (reproj1 z) . r = g1 . rlet r be
Element of
X;
(reproj1 z) . r = g1 . rreconsider r0 =
r as
Element of
(<*X,Y*> . (In (1,(dom <*X,Y*>)))) by AS1, FINSEQ_1:44;
In (1,
(dom <*X,Y*>))
in Seg 2
by AS1;
then
In (1,
(dom <*X,Y*>))
in Seg (len <*x,y*>)
by FINSEQ_1:44;
then X0:
In (1,
(dom <*X,Y*>))
in dom <*x,y*>
by FINSEQ_1:def 3;
X1:
R . r = <*x,y*> +* (
(In (1,(dom <*X,Y*>))),
r0)
by P4, NDIFF_5:def 4;
X3:
<*x,y*> +* (
(In (1,(dom <*X,Y*>))),
r0)
= <*x,y*> +* ((In (1,(dom <*X,Y*>))) .--> r0)
by FUNCT_7:def 3, X0;
X2:
<*x,y*> +* ((In (1,(dom <*X,Y*>))) .--> r0) = <*r,y*>
proof
set q =
<*x,y*> +* (1 .--> r0);
X5:
<*x,y*> +* (1 .--> r0) = <*x,y*> +* (1,
r0)
by AS1, X0, FUNCT_7:def 3;
then reconsider q =
<*x,y*> +* (1 .--> r0) as
FinSequence ;
K1:
len q =
len <*x,y*>
by X5, FUNCT_7:97
.=
2
by FINSEQ_1:44
;
1
in dom (1 .--> r0)
by FUNCOP_1:74;
then K3:
q . 1 =
(1 .--> r0) . 1
by FUNCT_4:13
.=
r
by FUNCOP_1:72
;
not 2
in dom (1 .--> r0)
by FUNCOP_1:75;
then q . 2 =
<*x,y*> . 2
by FUNCT_4:11
.=
y
by FINSEQ_1:44
;
hence
<*x,y*> +* ((In (1,(dom <*X,Y*>))) .--> r0) = <*r,y*>
by AS1, K1, K3, FINSEQ_1:44;
verum
end; g1 . r =
((IsoCPNrSP (X,Y)) ") . (R . r)
by FUNCT_2:15
.=
[r,y]
by X1, X2, X3, defISOA1
;
hence
(reproj1 z) . r = g1 . r
by P3, Defrep1;
verum end;
hence reproj1 z =
g1
.=
((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z)))
;
reproj2 z = ((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z)))
set f2 = reproj2 z;
<*X,Y*> . (In (2,(dom <*X,Y*>))) = Y
by AS2, FINSEQ_1:44;
then reconsider L = reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z)) as Function of Y,(product <*X,Y*>) ;
reconsider g2 = ((IsoCPNrSP (X,Y)) ") * L as Function of Y,[:X,Y:] ;
consider x being Point of X, y being Point of Y such that
P1:
z = [x,y]
by PRVECT_3:18;
P2:
z `1 = x
by P1;
P4: (IsoCPNrSP (X,Y)) . z =
(IsoCPNrSP (X,Y)) . (x,y)
by P1
.=
<*x,y*>
by defISO
;
now for r being Element of Y holds (reproj2 z) . r = g2 . rlet r be
Element of
Y;
(reproj2 z) . r = g2 . rreconsider r0 =
r as
Element of
(<*X,Y*> . (In (2,(dom <*X,Y*>)))) by AS2, FINSEQ_1:44;
In (2,
(dom <*X,Y*>))
in Seg 2
by AS2;
then
In (2,
(dom <*X,Y*>))
in Seg (len <*x,y*>)
by FINSEQ_1:44;
then X0:
In (2,
(dom <*X,Y*>))
in dom <*x,y*>
by FINSEQ_1:def 3;
X1:
L . r = <*x,y*> +* (
(In (2,(dom <*X,Y*>))),
r0)
by P4, NDIFF_5:def 4;
X3:
<*x,y*> +* (
(In (2,(dom <*X,Y*>))),
r0)
= <*x,y*> +* ((In (2,(dom <*X,Y*>))) .--> r0)
by FUNCT_7:def 3, X0;
X2:
<*x,y*> +* ((In (2,(dom <*X,Y*>))) .--> r0) = <*x,r*>
proof
set q =
<*x,y*> +* (2 .--> r0);
X5:
<*x,y*> +* (2 .--> r0) = <*x,y*> +* (2,
r0)
by AS2, X0, FUNCT_7:def 3;
then reconsider q =
<*x,y*> +* (2 .--> r0) as
FinSequence ;
K1:
len q =
len <*x,y*>
by X5, FUNCT_7:97
.=
2
by FINSEQ_1:44
;
2
in dom (2 .--> r0)
by FUNCOP_1:74;
then K3:
q . 2 =
(2 .--> r0) . 2
by FUNCT_4:13
.=
r
by FUNCOP_1:72
;
not 1
in dom (2 .--> r0)
by FUNCOP_1:75;
then q . 1 =
<*x,y*> . 1
by FUNCT_4:11
.=
x
by FINSEQ_1:44
;
hence
<*x,y*> +* ((In (2,(dom <*X,Y*>))) .--> r0) = <*x,r*>
by AS2, K1, K3, FINSEQ_1:44;
verum
end; g2 . r =
((IsoCPNrSP (X,Y)) ") . (L . r)
by FUNCT_2:15
.=
[x,r]
by X1, X2, X3, defISOA1
;
hence
(reproj2 z) . r = g2 . r
by P2, Defrep2;
verum end;
hence reproj2 z =
g2
.=
((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z)))
;
verum