let I be non empty non degenerated commutative multLoopStr_0 ; :: thesis: for u being Element of Q. I holds u in QClass. u
let u be Element of Q. I; :: thesis: u in QClass. u
(u `1 ) * (u `2 ) = (u `1 ) * (u `2 ) ;
hence u in QClass. u by Def4; :: thesis: verum