let e1, e2, e3, f1, f2, f3 be Element of F_Real; 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; 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); ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; ( ((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; ((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; verum