let X, Y be RealNormSpace; for z being Point of [:X,Y:] holds
( z `1 = (proj (In (1,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) & z `2 = (proj (In (2,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) )
let z be Point of [:X,Y:]; ( z `1 = (proj (In (1,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) & z `2 = (proj (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 G = <*X,Y*>;
AS3:
product <*X,Y*> = NORMSTR(# (product (carr <*X,Y*>)),(zeros <*X,Y*>),[:(addop <*X,Y*>):],[:(multop <*X,Y*>):],(productnorm <*X,Y*>) #)
by PRVECT_2:6;
consider x being Point of X, y being Point of Y such that
P1:
z = [x,y]
by PRVECT_3:18;
P4: (IsoCPNrSP (X,Y)) . z =
(IsoCPNrSP (X,Y)) . (x,y)
by P1
.=
<*x,y*>
by defISO
;
reconsider w = (IsoCPNrSP (X,Y)) . z as Element of product (carr <*X,Y*>) by AS3;
P5: (proj (In (1,(dom <*X,Y*>)))) . w =
<*x,y*> . 1
by P4, AS1, NDIFF_5:def 3
.=
z `1
by P1, FINSEQ_1:44
;
(proj (In (2,(dom <*X,Y*>)))) . w =
<*x,y*> . 2
by P4, AS2, NDIFF_5:def 3
.=
z `2
by P1, FINSEQ_1:44
;
hence
( z `1 = (proj (In (1,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) & z `2 = (proj (In (2,(dom <*X,Y*>)))) . ((IsoCPNrSP (X,Y)) . z) )
by P5; verum