let x, y be Element of R; :: thesis: ( ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & x = (b ^2) - ((4 '*' a) * c) ) & ex a being non zero Element of R ex b, c being Element of R st
( p = <%c,b,a%> & y = (b ^2) - ((4 '*' a) * c) ) implies x = y )
assume that
A1: ex a1 being non zero Element of R ex b1, c1 being Element of R st
( p = <%c1,b1,a1%> & x = (b1 ^2) - ((4 '*' a1) * c1) ) and
A2: ex a2 being non zero Element of R ex b2, c2 being Element of R st
( p = <%c2,b2,a2%> & y = (b2 ^2) - ((4 '*' a2) * c2) ) ; :: thesis: x = y
consider a1 being non zero Element of R, b1, c1 being Element of R such that
A3: ( p = <%c1,b1,a1%> & x = (b1 ^2) - ((4 '*' a1) * c1) ) by A1;
consider a2 being non zero Element of R, b2, c2 being Element of R such that
A4: ( p = <%c2,b2,a2%> & y = (b2 ^2) - ((4 '*' a2) * c2) ) by A2;
A5: a1 = <%c2,b2,a2%> . 2 by A3, A4, qua1
.= a2 by qua1 ;
A6: b1 = <%c2,b2,a2%> . 1 by A3, A4, qua1
.= b2 by qua1 ;
c1 = <%c2,b2,a2%> . 0 by A3, A4, qua1
.= c2 by qua1 ;
hence x = y by A5, A6, A3, A4; :: thesis: verum