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