let e1, e2, e3, f1, f2, f3 be Element of F_Real; :: thesis: for r1, r2 being Real
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 holds
( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p1) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p2) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )
let r1, r2 be Real; :: thesis: for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 holds
( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p1) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p2) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )
let p1, p2, p3, p4, p5, p6 be Point of (TOP-REAL 3); :: thesis: ( p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 implies ( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p1) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p2) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 ) )
assume that
A1: p1 = <*1,0,0*> and
A2: p2 = <*0,1,0*> and
A3: p3 = <*0,0,1*> and
A4: p4 = <*1,1,1*> and
A5: p5 = <*e1,e2,e3*> and
A6: p6 = <*f1,f2,f3*> and
A8: qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 and
A9: qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 ; :: thesis: ( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p1) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p2) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )
( p1 . 1 = 1 & p1 . 2 = 0 & p1 . 3 = 0 ) by A1, FINSEQ_1:45;
hence qfconic (0,0,0,r1,r2,(- (r1 + r2)),p1) = 0 ; :: thesis: ( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p2) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )
( p2 . 1 = 0 & p2 . 2 = 1 & p2 . 3 = 0 ) by A2, FINSEQ_1:45;
hence qfconic (0,0,0,r1,r2,(- (r1 + r2)),p2) = 0 ; :: thesis: ( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )
( p3 . 1 = 0 & p3 . 2 = 0 & p3 . 3 = 1 ) by A3, FINSEQ_1:45;
hence qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 ; :: thesis: ( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )
( p4 . 1 = 1 & p4 . 2 = 1 & p4 . 3 = 1 ) by A4, FINSEQ_1:45;
hence qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 ; :: thesis: ( ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )
( p5 . 1 = e1 & p5 . 2 = e2 & p5 . 3 = e3 ) by A5, FINSEQ_1:45;
hence ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 by A8; :: thesis: ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3
( p6 . 1 = f1 & p6 . 2 = f2 & p6 . 3 = f3 ) by A6, FINSEQ_1:45;
hence ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 by A9; :: thesis: verum