let n be non empty Element of NAT ; :: thesis: for i being Element of NAT
for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
(reproj i,y) * (proj 1,1) = reproj i,x
let i be Element of NAT ; :: thesis: for x being Point of (REAL-NS n)
for y being Element of REAL n st x = y holds
(reproj i,y) * (proj 1,1) = reproj i,x
let x be Point of (REAL-NS n); :: thesis: for y being Element of REAL n st x = y holds
(reproj i,y) * (proj 1,1) = reproj i,x
let y be Element of REAL n; :: thesis: ( x = y implies (reproj i,y) * (proj 1,1) = reproj i,x )
assume A1: x = y ; :: thesis: (reproj i,y) * (proj 1,1) = reproj i,x
A2: ( the carrier of (REAL-NS 1) = REAL 1 & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
reconsider k = proj 1,1 as Function of REAL 1, REAL ;

now

let s be Element of REAL 1; :: thesis: (reproj i,x) . s = ((reproj i,y) * k) . s
reconsider r = s as Point of (REAL-NS 1) by REAL_NS1:def 4;
consider q being Element of REAL , z being Element of REAL n such that
A3: ( r = <*q*> & z = x & (reproj i,x) . r = (reproj i,z) . q ) by Def6;
((reproj i,y) * k) . s = (reproj i,y) . (k . s) by FUNCT_2:21;
hence (reproj i,x) . s = ((reproj i,y) * k) . s by A1, A3, Lm1; :: thesis: verum

end;

hence (reproj i,y) * (proj 1,1) = reproj i,x by A2, FUNCT_2:113; :: thesis: verum