let m be non zero Nat; :: thesis: for x being Element of REAL
for i being Nat st 1 <= i & i <= m & x <> 0 holds
(reproj (i,(0* m))) . x <> 0* m
let x be Element of REAL ; :: thesis: for i being Nat st 1 <= i & i <= m & x <> 0 holds
(reproj (i,(0* m))) . x <> 0* m
let i be Nat; :: thesis: ( 1 <= i & i <= m & x <> 0 implies (reproj (i,(0* m))) . x <> 0* m )
assume ( 1 <= i & i <= m & x <> 0 ) ; :: thesis: (reproj (i,(0* m))) . x <> 0* m
then Replace ((0* m),i,x) <> 0* m by Th11;
hence (reproj (i,(0* m))) . x <> 0* m by PDIFF_1:def 5; :: thesis: verum