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