let m be non zero Nat; :: thesis: for x being Point of (REAL-NS 1)
for i being Nat st 1 <= i & i <= m & x <> 0. (REAL-NS 1) holds
(reproj (i,(0. (REAL-NS m)))) . x <> 0. (REAL-NS m)
let x be Point of (REAL-NS 1); :: thesis: for i being Nat st 1 <= i & i <= m & x <> 0. (REAL-NS 1) holds
(reproj (i,(0. (REAL-NS m)))) . x <> 0. (REAL-NS m)
let i be Nat; :: thesis: ( 1 <= i & i <= m & x <> 0. (REAL-NS 1) implies (reproj (i,(0. (REAL-NS m)))) . x <> 0. (REAL-NS m) )
assume A1: ( 1 <= i & i <= m & x <> 0. (REAL-NS 1) ) ; :: thesis: (reproj (i,(0. (REAL-NS m)))) . x <> 0. (REAL-NS m)
consider q1 being Element of REAL , z1 being Element of REAL m such that
A2: ( x = <*q1*> & z1 = 0. (REAL-NS m) & (reproj (i,(0. (REAL-NS m)))) . x = (reproj (i,z1)) . q1 ) by PDIFF_1:def 6;
A3: 0. (REAL-NS m) = 0* m by REAL_NS1:def 4;

now :: thesis: not q1 = 0

assume q1 = 0 ; :: thesis: contradiction
then <*q1*> = 0* 1 by FINSEQ_2:59;
hence contradiction by A2, A1, REAL_NS1:def 4; :: thesis: verum

end;

hence (reproj (i,(0. (REAL-NS m)))) . x <> 0. (REAL-NS m) by A2, A3, A1, Th17; :: thesis: verum