let X be RealLinearSpace-Sequence; :: thesis: 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; :: thesis: 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); :: thesis: for s being Function st x = s holds
(reproj (i,x)) . (s . i) = x
let s be Function; :: thesis: ( x = s implies (reproj (i,x)) . (s . i) = x )
assume A1: x = s ; :: thesis: (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; :: thesis: verum