let m be non empty Element of NAT ; :: thesis: for x being Element of REAL
for i being Element of 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 Element of NAT st 1 <= i & i <= m & x <> 0 holds
(reproj i,(0* m)) . x <> 0* m
let i be Element of 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