let I be non empty non degenerated multLoopStr_0 ; :: thesis: not Quot. I is empty
1. I <> 0. I ;
then reconsider u = [(1. I),(1. I)] as Element of Q. I by Def1;
QClass. u in Quot. I by Def5;
hence not Quot. I is empty ; :: thesis: verum