let X be RealNormSpace-Sequence; 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; 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); 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); for F being Function st F = (reproj (i,x)) . r holds
F . i = r
let F be Function; ( F = (reproj (i,x)) . r implies F . i = r )
assume A1:
F = (reproj (i,x)) . r
; 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 Def2;
thus
F . i = r
by A1, A2, A3, A4, Th1; verum