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