let X be RealLinearSpace-Sequence; :: thesis: for i being Element of dom X
for x being Element of (product X)
for r being Element of (X . i)
for F being Function st F = (reproj (i,x)) . r holds
F . i = r
let i be Element of dom X; :: thesis: for x being Element of (product X)
for r being Element of (X . i)
for F being Function st F = (reproj (i,x)) . r holds
F . i = r
let x be Element of (product X); :: thesis: for r being Element of (X . i)
for F being Function st F = (reproj (i,x)) . r holds
F . i = r
let r be Element of (X . i); :: thesis: for F being Function st F = (reproj (i,x)) . r holds
F . i = r
let F be Function; :: thesis: ( F = (reproj (i,x)) . r implies F . i = r )
assume A1: F = (reproj (i,x)) . r ; :: thesis: F . i = r
A2: dom (carr X) = dom X by LemmaX;
A3: (carr X) . i = the carrier of (X . i) by PRVECT_1:def 11;
consider x0 being Element of product (carr X) such that
A4: ( x0 = x & reproj (i,x) = reproj (i,x0) ) by Def20;
thus F . i = r by A1, A2, A3, A4, Th1; :: thesis: verum