let X be RealNormSpace; for s being Point of (product <*X*>)
for i being Element of dom <*X*> holds reproj (i,s) = IsoCPNrSP X
let s be Point of (product <*X*>); for i being Element of dom <*X*> holds reproj (i,s) = IsoCPNrSP X
let i be Element of dom <*X*>; reproj (i,s) = IsoCPNrSP X
A1:
i = 1
by FINSEQ_1:90;
A2:
<*X*> . i = X
by A1;
for x being Element of X holds (reproj (i,s)) . x = (IsoCPNrSP X) . x
proof
let x be
Element of
X;
(reproj (i,s)) . x = (IsoCPNrSP X) . x
s in the
carrier of
(product <*X*>)
;
then
s in rng (IsoCPNrSP X)
by FUNCT_2:def 3;
then consider x0 being
object such that A3:
(
x0 in the
carrier of
X &
s = (IsoCPNrSP X) . x0 )
by FUNCT_2:11;
reconsider x0 =
x0 as
Point of
X by A3;
A4:
(IsoCPNrSP X) . x0 = <*x0*>
by Def2;
dom s = Seg 1
by A3, A4, FINSEQ_1:38;
then A5:
i in dom s
by A1;
dom (s +* (i,x)) =
dom s
by FUNCT_7:30
.=
Seg 1
by A3, A4, FINSEQ_1:38
;
then A6:
len (s +* (i,x)) = 1
by FINSEQ_1:def 3;
A7:
(s +* (i,x)) . 1
= x
by A1, A5, FUNCT_7:31;
thus (reproj (i,s)) . x =
s +* (
i,
x)
by A2, NDIFF_5:def 4
.=
<*x*>
by A6, A7, FINSEQ_1:40
.=
(IsoCPNrSP X) . x
by Def2
;
verum
end;
hence
reproj (i,s) = IsoCPNrSP X
by A2; verum