let X be RealLinearSpace; for s being Point of (product <*X*>)
for i being Element of dom <*X*> holds reproj (i,s) = IsoCPRLSP X
let s be Point of (product <*X*>); for i being Element of dom <*X*> holds reproj (i,s) = IsoCPRLSP X
let i be Element of dom <*X*>; reproj (i,s) = IsoCPRLSP 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 = (IsoCPRLSP X) . x
proof
let x be
Element of
X;
(reproj (i,s)) . x = (IsoCPRLSP X) . x
s in the
carrier of
(product <*X*>)
;
then
s in rng (IsoCPRLSP X)
by FUNCT_2:def 3;
then consider y being
object such that A3:
(
y in the
carrier of
X &
s = (IsoCPRLSP X) . y )
by FUNCT_2:11;
reconsider y =
y as
Point of
X by A3;
A4:
(IsoCPRLSP X) . y = <*y*>
by Def1;
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, Th1
.=
<*x*>
by A6, A7, FINSEQ_1:40
.=
(IsoCPRLSP X) . x
by Def1
;
verum
end;
hence
reproj (i,s) = IsoCPRLSP X
by A2; verum