let m be non zero Nat; 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 ; 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; ( 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 )
; (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; verum