let m be non zero Nat; :: thesis: for x, y being Element of REAL
for i being 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 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 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)
reconsider xy = x + y as Element of REAL ;
( 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,xy) ) 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