let X be RealLinearSpace-Sequence; for i being Element of dom X
for x being Element of (product X)
for s being Function st x = s holds
(reproj (i,x)) . (s . i) = x
let i be Element of dom X; for x being Element of (product X)
for s being Function st x = s holds
(reproj (i,x)) . (s . i) = x
let x be Element of (product X); for s being Function st x = s holds
(reproj (i,x)) . (s . i) = x
let s be Function; ( x = s implies (reproj (i,x)) . (s . i) = x )
assume A1:
x = s
; (reproj (i,x)) . (s . i) = x
A2:
dom (carr X) = dom X
by LemmaX;
consider x0 being Element of product (carr X) such that
A4:
( x0 = x & reproj (i,x) = reproj (i,x0) )
by Def20;
thus
(reproj (i,x)) . (s . i) = x
by A1, A2, A4, Th2X; verum