let G be RealNormSpace-Sequence; :: thesis: for i being Element of dom G
for x being Point of (G . i) st x <> 0. (G . i) holds
(reproj (i,(0. (product G)))) . x <> 0. (product G)
let i be Element of dom G; :: thesis: for x being Point of (G . i) st x <> 0. (G . i) holds
(reproj (i,(0. (product G)))) . x <> 0. (product G)
let x be Point of (G . i); :: thesis: ( x <> 0. (G . i) implies (reproj (i,(0. (product G)))) . x <> 0. (product G) )
assume A1: x <> 0. (G . i) ; :: thesis: (reproj (i,(0. (product G)))) . x <> 0. (product G)
assume A2: (reproj (i,(0. (product G)))) . x = 0. (product G) ; :: thesis: contradiction
reconsider v = (reproj (i,(0. (product G)))) . x as Element of product (carr G) by Th10;
x = v . i by Th33;
hence contradiction by A1, Th14, A2; :: thesis: verum