let X, Y be RealNormSpace; :: thesis: 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:]; :: thesis: ( 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;
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 :: thesis: for r being Element of X holds (reproj1 z) . r = g1 . r

let r be Element of X; :: thesis: (reproj1 z) . r = g1 . r
reconsider r0 = r as Element of (<*X,Y*> . (In (1,(dom <*X,Y*>)))) by AS1;
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 ;
hence <*x,y*> +* ((In (1,(dom <*X,Y*>))) .--> r0) = <*r,y*> by AS1, K1, K3, FINSEQ_1:44; :: thesis: 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; :: thesis: verum

end;

hence reproj1 z = g1
.= ((IsoCPNrSP (X,Y)) ") * (reproj ((In (1,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) ;
:: thesis: 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;
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 :: thesis: for r being Element of Y holds (reproj2 z) . r = g2 . r

let r be Element of Y; :: thesis: (reproj2 z) . r = g2 . r
reconsider r0 = r as Element of (<*X,Y*> . (In (2,(dom <*X,Y*>)))) by AS2;
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 ;
hence <*x,y*> +* ((In (2,(dom <*X,Y*>))) .--> r0) = <*x,r*> by AS2, K1, K3, FINSEQ_1:44; :: thesis: 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; :: thesis: verum

end;

hence reproj2 z = g2
.= ((IsoCPNrSP (X,Y)) ") * (reproj ((In (2,(dom <*X,Y*>))),((IsoCPNrSP (X,Y)) . z))) ;
:: thesis: verum