let I be non empty non degenerated multLoopStr_0 ; :: thesis: for u being Element of Q. I holds u `2 <> 0. I
let u be Element of Q. I; :: thesis: u `2 <> 0. I
ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) by Def1;
hence u `2 <> 0. I ; :: thesis: verum