let n be non zero Nat; :: thesis: for i being 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 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) )

reconsider k = proj (1,1) as Function of (REAL 1),REAL ;

A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

assume A2: x = y ; :: thesis: (reproj (i,y)) * (proj (1,1)) = reproj (i,x)

hence (reproj (i,y)) * (proj (1,1)) = reproj (i,x) by A1, A3, FUNCT_2:63; :: thesis: verum

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 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) )

reconsider k = proj (1,1) as Function of (REAL 1),REAL ;

A1: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;

assume A2: x = y ; :: thesis: (reproj (i,y)) * (proj (1,1)) = reproj (i,x)

A3: now :: thesis: for s being Element of REAL 1 holds (reproj (i,x)) . s = ((reproj (i,y)) * k) . s

the carrier of (REAL-NS 1) = REAL 1
by REAL_NS1:def 4;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;

A4: ((reproj (i,y)) * k) . s = (reproj (i,y)) . (k . s) by FUNCT_2:15;

ex q being Element of REAL ex z being Element of REAL n st

( r = <*q*> & z = x & (reproj (i,x)) . r = (reproj (i,z)) . q ) by Def6;

hence (reproj (i,x)) . s = ((reproj (i,y)) * k) . s by A2, A4, Lm1; :: thesis: verum

end;reconsider r = s as Point of (REAL-NS 1) by REAL_NS1:def 4;

A4: ((reproj (i,y)) * k) . s = (reproj (i,y)) . (k . s) by FUNCT_2:15;

ex q being Element of REAL ex z being Element of REAL n st

( r = <*q*> & z = x & (reproj (i,x)) . r = (reproj (i,z)) . q ) by Def6;

hence (reproj (i,x)) . s = ((reproj (i,y)) * k) . s by A2, A4, Lm1; :: thesis: verum

hence (reproj (i,y)) * (proj (1,1)) = reproj (i,x) by A1, A3, FUNCT_2:63; :: thesis: verum