let m be non zero Nat; :: thesis: for x, a being Real
for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0* m))) . (a * x) = a (#) ((reproj (i,(0* m))) . x)
let x, a be Real; :: thesis: for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0* m))) . (a * x) = a (#) ((reproj (i,(0* m))) . x)
let i be Nat; :: thesis: ( 1 <= i & i <= m implies (reproj (i,(0* m))) . (a * x) = a (#) ((reproj (i,(0* m))) . x) )
assume A1: ( 1 <= i & i <= m ) ; :: thesis: (reproj (i,(0* m))) . (a * x) = a (#) ((reproj (i,(0* m))) . x)
reconsider a = a, x = x as Element of REAL by XREAL_0:def 1;
reconsider ax = a * x as Element of REAL ;
A2: Replace ((0* m),i,ax) = a * (Replace ((0* m),i,x)) by Th10, A1;
Replace ((0* m),i,x) = (reproj (i,(0* m))) . x by PDIFF_1:def 5;
then (reproj (i,(0* m))) . (a * x) = a * ((reproj (i,(0* m))) . x) by A2, PDIFF_1:def 5;
hence (reproj (i,(0* m))) . (a * x) = a (#) ((reproj (i,(0* m))) . x) ; :: thesis: verum