let m be non zero Nat; :: thesis: for x, y being Element of REAL
for z being Element of REAL m
for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0* m))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0* m))) . (y - x) )
let x, y be Element of REAL ; :: thesis: for z being Element of REAL m
for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0* m))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0* m))) . (y - x) )
let z be Element of REAL m; :: thesis: for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0* m))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0* m))) . (y - x) )
let i be Nat; :: thesis: ( 1 <= i & i <= m & y = (proj (i,m)) . z implies ( ((reproj (i,z)) . x) - z = (reproj (i,(0* m))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0* m))) . (y - x) ) )
reconsider xy = x - y, yx = y - x as Element of REAL ;
assume ( 1 <= i & i <= m & y = (proj (i,m)) . z ) ; :: thesis: ( ((reproj (i,z)) . x) - z = (reproj (i,(0* m))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0* m))) . (y - x) )
then A1: ( (Replace (z,i,x)) - z = Replace ((0* m),i,xy) & z - (Replace (z,i,x)) = Replace ((0* m),i,yx) ) by Th12;
Replace (z,i,x) = (reproj (i,z)) . x by PDIFF_1:def 5;
hence ( ((reproj (i,z)) . x) - z = (reproj (i,(0* m))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0* m))) . (y - x) ) by A1, PDIFF_1:def 5; :: thesis: verum