let X be RealNormSpace-Sequence; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum