let m be non empty Element of NAT ; :: thesis: for x, y being Element of REAL
for z being Element of REAL m
for i being Element of 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 Element of 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 Element of 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 Element of 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) ) )
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,(x - y) & z - (Replace z,i,x) = Replace (0* m),i,(y - x) ) 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