let X be RealNormSpace-Sequence; for i, j being Element of dom X
for x being Element of (product X)
for r being Element of (X . i)
for F, s being Function st F = (reproj (i,x)) . r & x = s & i <> j holds
F . j = s . j
let i, j be Element of dom X; for x being Element of (product X)
for r being Element of (X . i)
for F, s being Function st F = (reproj (i,x)) . r & x = s & i <> j holds
F . j = s . j
let x be Element of (product X); for r being Element of (X . i)
for F, s being Function st F = (reproj (i,x)) . r & x = s & i <> j holds
F . j = s . j
let r be Element of (X . i); for F, s being Function st F = (reproj (i,x)) . r & x = s & i <> j holds
F . j = s . j
let F, s be Function; ( F = (reproj (i,x)) . r & x = s & i <> j implies F . j = s . j )
assume A1:
( F = (reproj (i,x)) . r & x = s & i <> j )
; F . j = s . j
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 . j = s . j
by A1, A2, A3, A4, Th2; verum