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