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