consider y being Element of Q. I such that
A1: v = QClass. y by Def5;
consider x being Element of Q. I such that
A2: u = QClass. x by Def5;
( x `2 <> 0. I & y `2 <> 0. I ) by Th2;
then (x `2) * (y `2) <> 0. I by VECTSP_2:def 1;
then reconsider t = [((x `1) * (y `1)),((x `2) * (y `2))] as Element of Q. I by Def1;
set M = QClass. t;
A3: for z being Element of Q. I st z in QClass. t holds
ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) )
proof
let z be Element of Q. I; :: thesis: ( z in QClass. t implies ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) )
assume z in QClass. t ; :: thesis: ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) )
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then (z `1) * (t `2) = (z `2) * ((x `1) * (y `1)) ;
then A4: (z `1) * ((x `2) * (y `2)) = (z `2) * ((x `1) * (y `1)) ;
x in u by A2, Th5;
hence ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) by A1, A4, Th5; :: thesis: verum
end;
A5: for z being Element of Q. I st ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) holds
z in QClass. t
proof
let z be Element of Q. I; :: thesis: ( ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) implies z in QClass. t )
given a, b being Element of Q. I such that A6: a in u and
A7: b in v and
A8: (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ; :: thesis: z in QClass. t
A9: (a `1) * (x `2) = (a `2) * (x `1) by A2, A6, Def4;
A10: (b `1) * (y `2) = (b `2) * (y `1) by A1, A7, Def4;
( a `2 <> 0. I & b `2 <> 0. I ) by Th2;
then A11: (a `2) * (b `2) <> 0. I by VECTSP_2:def 1;
A12: (a `2) * (b `2) divides (z `2) * ((a `1) * (b `1)) by A8, GCD_1:def 1;
then A13: (a `2) * (b `2) divides ((z `2) * ((a `1) * (b `1))) * ((x `2) * (y `2)) by GCD_1:7;
(a `2) * (b `2) divides (a `2) * (b `2) ;
then (a `2) * (b `2) divides ((z `2) * ((x `1) * (y `1))) * ((a `2) * (b `2)) by GCD_1:7;
then A14: (((z `2) * ((x `1) * (y `1))) * ((a `2) * (b `2))) / ((a `2) * (b `2)) = ((z `2) * ((x `1) * (y `1))) * (((a `2) * (b `2)) / ((a `2) * (b `2))) by A11, GCD_1:11
.= ((z `2) * ((x `1) * (y `1))) * (1_ I) by A11, GCD_1:9
.= (z `2) * ((x `1) * (y `1)) ;
((z `2) * ((a `1) * (b `1))) / ((a `2) * (b `2)) = z `1 by A8, A12, A11, GCD_1:def 4;
then (z `1) * ((x `2) * (y `2)) = (((z `2) * ((a `1) * (b `1))) * ((x `2) * (y `2))) / ((a `2) * (b `2)) by A12, A11, A13, GCD_1:11
.= ((z `2) * (((a `1) * (b `1)) * ((x `2) * (y `2)))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((a `1) * ((b `1) * ((x `2) * (y `2))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((a `1) * ((x `2) * ((b `1) * (y `2))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * (((a `2) * (x `1)) * ((b `1) * (y `2)))) / ((a `2) * (b `2)) by A9, GROUP_1:def 3
.= ((z `2) * ((x `1) * ((a `2) * ((b `2) * (y `1))))) / ((a `2) * (b `2)) by A10, GROUP_1:def 3
.= ((z `2) * ((x `1) * ((y `1) * ((a `2) * (b `2))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * (((x `1) * (y `1)) * ((a `2) * (b `2)))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= (((z `2) * ((x `1) * (y `1))) * ((a `2) * (b `2))) / ((a `2) * (b `2)) by GROUP_1:def 3 ;
then (z `1) * (t `2) = (z `2) * ((x `1) * (y `1)) by A14
.= (z `2) * (t `1) ;
hence z in QClass. t by Def4; :: thesis: verum
end;
QClass. t is Element of Quot. I by Def5;
hence ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) by A5, A3; :: thesis: verum