let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v, w being Element of Quot. I holds qmult (u,(qadd (v,w))) = qadd ((qmult (u,v)),(qmult (u,w)))
let u, v, w be Element of Quot. I; :: thesis: qmult (u,(qadd (v,w))) = qadd ((qmult (u,v)),(qmult (u,w)))
consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
consider y being Element of Q. I such that
A2: v = QClass. y by Def5;
consider z being Element of Q. I such that
A3: w = QClass. z by Def5;
A4: x `2 <> 0. I by Th2;
A5: z `2 <> 0. I by Th2;
then A6: (x `2) * (z `2) <> 0. I by A4, VECTSP_2:def 1;
then reconsider s2 = [((x `1) * (z `1)),((x `2) * (z `2))] as Element of Q. I by Def1;
A7: y `2 <> 0. I by Th2;
then A8: (y `2) * (z `2) <> 0. I by A5, VECTSP_2:def 1;
then reconsider s = [(((y `1) * (z `2)) + ((z `1) * (y `2))),((y `2) * (z `2))] as Element of Q. I by Def1;
A9: (x `2) * (y `2) <> 0. I by A4, A7, VECTSP_2:def 1;
then reconsider s1 = [((x `1) * (y `1)),((x `2) * (y `2))] as Element of Q. I by Def1;
((x `2) * (y `2)) * ((x `2) * (z `2)) <> 0. I by A9, A6, VECTSP_2:def 1;
then reconsider s3 = [((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))),(((x `2) * (y `2)) * ((x `2) * (z `2)))] as Element of Q. I by Def1;
(x `2) * ((y `2) * (z `2)) <> 0. I by A4, A8, VECTSP_2:def 1;
then reconsider r = [((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))),((x `2) * ((y `2) * (z `2)))] as Element of Q. I by Def1;
A10: for t being Element of Q. I st t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) holds
t in QClass. (pmult (x,(padd (y,z))))

proof

let t be Element of Q. I; :: thesis: ( t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) implies t in QClass. (pmult (x,(padd (y,z)))) )
assume t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) ; :: thesis: t in QClass. (pmult (x,(padd (y,z))))
then (t `1) * (s3 `2) = (t `2) * (s3 `1) by Def4;
then (t `1) * (((x `2) * (y `2)) * ((x `2) * (z `2))) = (t `2) * (s3 `1) ;
then A11: (t `1) * (((x `2) * (y `2)) * ((x `2) * (z `2))) = (t `2) * ((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))) ;
((t `1) * ((x `2) * ((y `2) * (z `2)))) * (x `2) = ((t `1) * (((x `2) * (y `2)) * (z `2))) * (x `2) by GROUP_1:def 3
.= (t `1) * ((((x `2) * (y `2)) * (z `2)) * (x `2)) by GROUP_1:def 3
.= (t `2) * ((((x `1) * (y `1)) * ((x `2) * (z `2))) + (((x `1) * (z `1)) * ((x `2) * (y `2)))) by A11, GROUP_1:def 3
.= (t `2) * (((((x `1) * (y `1)) * (z `2)) * (x `2)) + (((x `1) * (z `1)) * ((x `2) * (y `2)))) by GROUP_1:def 3
.= (t `2) * (((((x `1) * (y `1)) * (z `2)) * (x `2)) + ((((x `1) * (z `1)) * (y `2)) * (x `2))) by GROUP_1:def 3
.= (t `2) * (((((x `1) * (y `1)) * (z `2)) + (((x `1) * (z `1)) * (y `2))) * (x `2)) by VECTSP_1:def 3
.= (t `2) * ((((x `1) * ((y `1) * (z `2))) + (((x `1) * (z `1)) * (y `2))) * (x `2)) by GROUP_1:def 3
.= (t `2) * ((((x `1) * ((y `1) * (z `2))) + ((x `1) * ((z `1) * (y `2)))) * (x `2)) by GROUP_1:def 3
.= (t `2) * (((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) * (x `2)) by VECTSP_1:def 2
.= ((t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2))))) * (x `2) by GROUP_1:def 3 ;
then (t `1) * ((x `2) * ((y `2) * (z `2))) = (t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) by A4, GCD_1:1;
then (t `1) * (r `2) = (t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2))))
.= (t `2) * (r `1) ;
hence t in QClass. (pmult (x,(padd (y,z)))) by Def4; :: thesis: verum

end;

A12: for t being Element of Q. I st t in QClass. (pmult (x,(padd (y,z)))) holds
t in QClass. (padd ((pmult (x,y)),(pmult (x,z))))

proof

let t be Element of Q. I; :: thesis: ( t in QClass. (pmult (x,(padd (y,z)))) implies t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) )
assume t in QClass. (pmult (x,(padd (y,z)))) ; :: thesis: t in QClass. (padd ((pmult (x,y)),(pmult (x,z))))
then (t `1) * (r `2) = (t `2) * (r `1) by Def4;
then (t `1) * ((x `2) * ((y `2) * (z `2))) = (t `2) * (r `1) ;
then A13: (t `1) * ((x `2) * ((y `2) * (z `2))) = (t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) ;
(t `1) * (s3 `2) = (t `1) * (((x `2) * (y `2)) * ((x `2) * (z `2)))
.= (t `1) * ((((x `2) * (y `2)) * (z `2)) * (x `2)) by GROUP_1:def 3
.= ((t `1) * (((x `2) * (y `2)) * (z `2))) * (x `2) by GROUP_1:def 3
.= ((t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2))))) * (x `2) by A13, GROUP_1:def 3
.= (t `2) * (((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2)))) * (x `2)) by GROUP_1:def 3
.= (t `2) * ((((x `1) * ((y `1) * (z `2))) + ((x `1) * ((z `1) * (y `2)))) * (x `2)) by VECTSP_1:def 2
.= (t `2) * ((((x `1) * ((y `1) * (z `2))) * (x `2)) + (((x `1) * ((z `1) * (y `2))) * (x `2))) by VECTSP_1:def 3
.= (t `2) * (((((x `1) * (y `1)) * (z `2)) * (x `2)) + (((x `1) * ((z `1) * (y `2))) * (x `2))) by GROUP_1:def 3
.= (t `2) * ((((x `1) * (y `1)) * ((z `2) * (x `2))) + (((x `1) * ((z `1) * (y `2))) * (x `2))) by GROUP_1:def 3
.= (t `2) * ((((x `1) * (y `1)) * ((z `2) * (x `2))) + ((((x `1) * (z `1)) * (y `2)) * (x `2))) by GROUP_1:def 3
.= (t `2) * ((((x `1) * (y `1)) * ((z `2) * (x `2))) + (((x `1) * (z `1)) * ((y `2) * (x `2)))) by GROUP_1:def 3
.= (t `2) * (s3 `1) ;
hence t in QClass. (padd ((pmult (x,y)),(pmult (x,z)))) by Def4; :: thesis: verum

end;

A14: qmult (u,(qadd (v,w))) = qmult ((QClass. x),(QClass. (padd (y,z)))) by A1, A2, A3, Th9
.= QClass. (pmult (x,(padd (y,z)))) by Th10 ;
qadd ((qmult (u,v)),(qmult (u,w))) = qadd ((QClass. (pmult (x,y))),(qmult ((QClass. x),(QClass. z)))) by A1, A2, A3, Th10
.= qadd ((QClass. (pmult (x,y))),(QClass. (pmult (x,z)))) by Th10
.= QClass. (padd ((pmult (x,y)),(pmult (x,z)))) by Th9 ;
hence qmult (u,(qadd (v,w))) = qadd ((qmult (u,v)),(qmult (u,w))) by A14, A12, A10, SUBSET_1:3; :: thesis: verum