let f, g be Function of (REAL-NS 1),(REAL-NS n); :: thesis: ( ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & f . r = (reproj (i,y)) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & g . r = (reproj (i,y)) . q ) ) implies f = g )

assume that

A3: for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & f . r = (reproj (i,y)) . q ) and

A4: for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & g . r = (reproj (i,y)) . q ) ; :: thesis: f = g

( r = <*q*> & y = x & f . r = (reproj (i,y)) . q ) ) & ( for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & g . r = (reproj (i,y)) . q ) ) implies f = g )

assume that

A3: for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & f . r = (reproj (i,y)) . q ) and

A4: for r being Element of (REAL-NS 1) ex q being Element of REAL ex y being Element of REAL n st

( r = <*q*> & y = x & g . r = (reproj (i,y)) . q ) ; :: thesis: f = g

now :: thesis: for r being Point of (REAL-NS 1) holds f . r = g . r

hence
f = g
by FUNCT_2:63; :: thesis: verumlet r be Point of (REAL-NS 1); :: thesis: f . r = g . r

consider p being Element of REAL , y being Element of REAL n such that

A5: r = <*p*> and

A6: y = x and

A7: f . r = (reproj (i,y)) . p by A3;

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

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

p = <*p*> . 1 by FINSEQ_1:def 8;

hence f . r = g . r by A5, A6, A7, A8, FINSEQ_1:def 8; :: thesis: verum

end;consider p being Element of REAL , y being Element of REAL n such that

A5: r = <*p*> and

A6: y = x and

A7: f . r = (reproj (i,y)) . p by A3;

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

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

p = <*p*> . 1 by FINSEQ_1:def 8;

hence f . r = g . r by A5, A6, A7, A8, FINSEQ_1:def 8; :: thesis: verum