let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v being Element of Q. I holds qadd (QClass. u),(QClass. v) = QClass. (padd u,v)
let u, v be Element of Q. I; :: thesis: qadd (QClass. u),(QClass. v) = QClass. (padd 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 `2 )) + ((v `1 ) * (u `2 ))),((u `2 ) * (v `2 ))] as Element of Q. I by Def1;
A1: ( w `1 = ((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 )) & 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 qadd (QClass. u),(QClass. v) holds
z in QClass. (padd u,v)

proof

let z be Element of Q. I; :: thesis: ( z in qadd (QClass. u),(QClass. v) implies z in QClass. (padd u,v) )
assume z in qadd (QClass. u),(QClass. v) ; :: thesis: z in QClass. (padd 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 `2 )) + ((b `1 ) * (a `2 ))) by Def6;
A6: (a `1 ) * (u `2 ) = (a `2 ) * (u `1 ) by A3, Def4;
A7: (b `1 ) * (v `2 ) = (b `2 ) * (v `1 ) by A4, Def4;
(a `2 ) * (b `2 ) divides (a `2 ) * (b `2 ) ;
then A8: (a `2 ) * (b `2 ) divides ((z `2 ) * (((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 )))) * ((a `2 ) * (b `2 )) by GCD_1:7;
A9: (a `2 ) * (b `2 ) divides (z `2 ) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) by A5, GCD_1:def 1;
then A10: (a `2 ) * (b `2 ) divides ((z `2 ) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )))) * ((u `2 ) * (v `2 )) by GCD_1:7;
( a `2 <> 0. I & b `2 <> 0. I ) by Th2;
then A11: (a `2 ) * (b `2 ) <> 0. I by VECTSP_2:def 5;
then z `1 = ((z `2 ) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )))) / ((a `2 ) * (b `2 )) by A5, A9, GCD_1:def 4;
then (z `1 ) * ((u `2 ) * (v `2 )) = (((z `2 ) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 )))) * ((u `2 ) * (v `2 ))) / ((a `2 ) * (b `2 )) by A11, A9, A10, GCD_1:11
.= ((z `2 ) * ((((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) * ((u `2 ) * (v `2 )))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((((a `1 ) * (b `2 )) * ((u `2 ) * (v `2 ))) + (((b `1 ) * (a `2 )) * ((u `2 ) * (v `2 ))))) / ((a `2 ) * (b `2 )) by VECTSP_1:def 12
.= ((z `2 ) * (((b `2 ) * ((a `1 ) * ((u `2 ) * (v `2 )))) + (((b `1 ) * (a `2 )) * ((u `2 ) * (v `2 ))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * (((b `2 ) * (((a `2 ) * (u `1 )) * (v `2 ))) + (((b `1 ) * (a `2 )) * ((u `2 ) * (v `2 ))))) / ((a `2 ) * (b `2 )) by A6, GROUP_1:def 4
.= ((z `2 ) * (((b `2 ) * (((a `2 ) * (u `1 )) * (v `2 ))) + ((a `2 ) * ((b `1 ) * ((v `2 ) * (u `2 )))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * (((b `2 ) * (((a `2 ) * (u `1 )) * (v `2 ))) + ((a `2 ) * (((b `2 ) * (v `1 )) * (u `2 ))))) / ((a `2 ) * (b `2 )) by A7, GROUP_1:def 4
.= ((z `2 ) * ((((b `2 ) * ((a `2 ) * (u `1 ))) * (v `2 )) + ((a `2 ) * (((b `2 ) * (v `1 )) * (u `2 ))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((((u `1 ) * ((b `2 ) * (a `2 ))) * (v `2 )) + ((a `2 ) * (((b `2 ) * (v `1 )) * (u `2 ))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((((u `1 ) * (v `2 )) * ((b `2 ) * (a `2 ))) + ((a `2 ) * (((b `2 ) * (v `1 )) * (u `2 ))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((((u `1 ) * (v `2 )) * ((b `2 ) * (a `2 ))) + (((a `2 ) * ((b `2 ) * (v `1 ))) * (u `2 )))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((((u `1 ) * (v `2 )) * ((a `2 ) * (b `2 ))) + (((v `1 ) * ((a `2 ) * (b `2 ))) * (u `2 )))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((((u `1 ) * (v `2 )) * ((a `2 ) * (b `2 ))) + (((v `1 ) * (u `2 )) * ((a `2 ) * (b `2 ))))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * ((((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 ))) * ((a `2 ) * (b `2 )))) / ((a `2 ) * (b `2 )) by VECTSP_1:def 12
.= (((z `2 ) * (((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 )))) * ((a `2 ) * (b `2 ))) / ((a `2 ) * (b `2 )) by GROUP_1:def 4
.= ((z `2 ) * (((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 )))) * (((a `2 ) * (b `2 )) / ((a `2 ) * (b `2 ))) by A11, A8, GCD_1:11
.= ((z `2 ) * (((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 )))) * (1_ I) by A11, GCD_1:9
.= (z `2 ) * (((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 ))) by VECTSP_1:def 13 ;
hence z in QClass. (padd u,v) by A1, Def4; :: thesis: verum

end;

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

proof

let z be Element of Q. I; :: thesis: ( z in QClass. (padd u,v) implies z in qadd (QClass. u),(QClass. v) )
assume z in QClass. (padd u,v) ; :: thesis: z in qadd (QClass. u),(QClass. v)
then A12: (z `1 ) * ((u `2 ) * (v `2 )) = (z `2 ) * (((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 ))) by A1, Def4;
( u in QClass. u & v in QClass. v ) by Th6;
hence z in qadd (QClass. u),(QClass. v) by A12, Def6; :: thesis: verum

end;

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