let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v being Element of Q. I holds qmult (QClass. u),(QClass. v) = QClass. (pmult u,v)
let u, v be Element of Q. I; :: thesis: qmult (QClass. u),(QClass. v) = QClass. (pmult u,v)
( u `2 <> 0. I & v `2 <> 0. I ) by Th2;
then (u `2 ) * (v `2 ) <> 0. I by VECTSP_2:def 5;
then reconsider w = [((u `1 ) * (v `1 )),((u `2 ) * (v `2 ))] as Element of Q. I by Def1;
A1: ( w `1 = (u `1 ) * (v `1 ) & w `2 = (u `2 ) * (v `2 ) ) by MCART_1:def 1, MCART_1:def 2;
A2: for z being Element of Q. I st z in qmult (QClass. u),(QClass. v) holds
z in QClass. (pmult u,v)

proof

let z be Element of Q. I; :: thesis: ( z in qmult (QClass. u),(QClass. v) implies z in QClass. (pmult u,v) )
assume z in qmult (QClass. u),(QClass. v) ; :: thesis: z in QClass. (pmult u,v)
then consider a, b being Element of Q. I such that
A3: a in QClass. u and
A4: b in QClass. v and
A5: (z `1 ) * ((a `2 ) * (b `2 )) = (z `2 ) * ((a `1 ) * (b `1 )) by Def7;
A6: (b `1 ) * (v `2 ) = (b `2 ) * (v `1 ) by A4, Def4;
A7: (a `1 ) * (u `2 ) = (a `2 ) * (u `1 ) by A3, Def4;

now

per cases ( a `1 = 0. I or b `1 = 0. I or ( a `1 <> 0. I & b `1 <> 0. I ) ) ;

case A8: a `1 = 0. I ; :: thesis: z in QClass. (pmult u,v)

then (a `1 ) * (b `1 ) = 0. I by VECTSP_1:39;
then A9: (z `2 ) * ((a `1 ) * (b `1 )) = 0. I by VECTSP_1:39;
A10: a `2 <> 0. I by Th2;
b `2 <> 0. I by Th2;
then (a `2 ) * (b `2 ) <> 0. I by A10, VECTSP_2:def 5;
then A11: z `1 = 0. I by A5, A9, VECTSP_2:def 5;
(a `1 ) * (u `2 ) = 0. I by A8, VECTSP_1:39;
then u `1 = 0. I by A7, A10, VECTSP_2:def 5;
then (z `2 ) * ((u `1 ) * (v `1 )) = (z `2 ) * (0. I) by VECTSP_1:39
.= 0. I by VECTSP_1:39
.= (z `1 ) * ((u `2 ) * (v `2 )) by A11, VECTSP_1:39 ;
hence z in QClass. (pmult u,v) by A1, Def4; :: thesis: verum

end;

case A12: b `1 = 0. I ; :: thesis: z in QClass. (pmult u,v)

then (a `1 ) * (b `1 ) = 0. I by VECTSP_1:39;
then A13: (z `2 ) * ((a `1 ) * (b `1 )) = 0. I by VECTSP_1:39;
A14: b `2 <> 0. I by Th2;
a `2 <> 0. I by Th2;
then (a `2 ) * (b `2 ) <> 0. I by A14, VECTSP_2:def 5;
then A15: z `1 = 0. I by A5, A13, VECTSP_2:def 5;
(b `1 ) * (v `2 ) = 0. I by A12, VECTSP_1:39;
then v `1 = 0. I by A6, A14, VECTSP_2:def 5;
then (z `2 ) * ((u `1 ) * (v `1 )) = (z `2 ) * (0. I) by VECTSP_1:39
.= 0. I by VECTSP_1:39
.= (z `1 ) * ((u `2 ) * (v `2 )) by A15, VECTSP_1:39 ;
hence z in QClass. (pmult u,v) by A1, Def4; :: thesis: verum

end;

case A16: ( a `1 <> 0. I & b `1 <> 0. I ) ; :: thesis: z in QClass. (pmult u,v)

(a `1 ) * (b `1 ) divides (a `1 ) * (b `1 ) ;
then A17: (a `1 ) * (b `1 ) divides (((z `2 ) * (u `1 )) * (v `1 )) * ((a `1 ) * (b `1 )) by GCD_1:7;
A18: (a `1 ) * (b `1 ) <> 0. I by A16, VECTSP_2:def 5;
A19: b `1 divides (b `2 ) * (v `1 ) by A6, GCD_1:def 1;
then A20: v `2 = ((b `2 ) * (v `1 )) / (b `1 ) by A6, A16, GCD_1:def 4;
A21: a `1 divides (a `2 ) * (u `1 ) by A7, GCD_1:def 1;
then A22: (a `1 ) * (b `1 ) divides ((a `2 ) * (u `1 )) * ((b `2 ) * (v `1 )) by A19, GCD_1:3;
then A23: (a `1 ) * (b `1 ) divides (z `1 ) * (((a `2 ) * (u `1 )) * ((b `2 ) * (v `1 ))) by GCD_1:7;
u `2 = ((a `2 ) * (u `1 )) / (a `1 ) by A7, A16, A21, GCD_1:def 4;
then (z `1 ) * ((u `2 ) * (v `2 )) = (z `1 ) * ((((a `2 ) * (u `1 )) * ((b `2 ) * (v `1 ))) / ((a `1 ) * (b `1 ))) by A16, A21, A19, A20, GCD_1:14
.= ((z `1 ) * (((a `2 ) * (u `1 )) * ((b `2 ) * (v `1 )))) / ((a `1 ) * (b `1 )) by A18, A22, A23, GCD_1:11
.= ((z `1 ) * ((((u `1 ) * (a `2 )) * (b `2 )) * (v `1 ))) / ((a `1 ) * (b `1 )) by GROUP_1:def 4
.= ((z `1 ) * ((((a `2 ) * (b `2 )) * (u `1 )) * (v `1 ))) / ((a `1 ) * (b `1 )) by GROUP_1:def 4
.= (((z `1 ) * (((a `2 ) * (b `2 )) * (u `1 ))) * (v `1 )) / ((a `1 ) * (b `1 )) by GROUP_1:def 4
.= ((((z `2 ) * ((a `1 ) * (b `1 ))) * (u `1 )) * (v `1 )) / ((a `1 ) * (b `1 )) by A5, GROUP_1:def 4
.= ((((z `2 ) * (u `1 )) * ((a `1 ) * (b `1 ))) * (v `1 )) / ((a `1 ) * (b `1 )) by GROUP_1:def 4
.= ((((z `2 ) * (u `1 )) * (v `1 )) * ((a `1 ) * (b `1 ))) / ((a `1 ) * (b `1 )) by GROUP_1:def 4
.= (((z `2 ) * (u `1 )) * (v `1 )) * (((a `1 ) * (b `1 )) / ((a `1 ) * (b `1 ))) by A18, A17, GCD_1:11
.= (((z `2 ) * (u `1 )) * (v `1 )) * (1_ I) by A18, GCD_1:9
.= ((z `2 ) * (u `1 )) * (v `1 ) by VECTSP_1:def 13
.= (z `2 ) * ((u `1 ) * (v `1 )) by GROUP_1:def 4 ;
hence z in QClass. (pmult u,v) by A1, Def4; :: thesis: verum

end;

end;

end;

hence z in QClass. (pmult u,v) ; :: thesis: verum

end;

for z being Element of Q. I st z in QClass. (pmult u,v) holds
z in qmult (QClass. u),(QClass. v)

proof

let z be Element of Q. I; :: thesis: ( z in QClass. (pmult u,v) implies z in qmult (QClass. u),(QClass. v) )
assume z in QClass. (pmult u,v) ; :: thesis: z in qmult (QClass. u),(QClass. v)
then A24: (z `1 ) * ((u `2 ) * (v `2 )) = (z `2 ) * ((u `1 ) * (v `1 )) by A1, Def4;
( u in QClass. u & v in QClass. v ) by Th6;
hence z in qmult (QClass. u),(QClass. v) by A24, Def7; :: thesis: verum

end;

hence qmult (QClass. u),(QClass. v) = QClass. (pmult u,v) by A2, SUBSET_1:8; :: thesis: verum