let Q be multLoop; :: thesis: for H being SubLoop of Q
for x, y being Element of Q
for x1, y1 being Element of H st x = x1 & y = y1 holds
x / y = x1 / y1
let H be SubLoop of Q; :: thesis: for x, y being Element of Q
for x1, y1 being Element of H st x = x1 & y = y1 holds
x / y = x1 / y1
let x, y be Element of Q; :: thesis: for x1, y1 being Element of H st x = x1 & y = y1 holds
x / y = x1 / y1
let x1, y1 be Element of H; :: thesis: ( x = x1 & y = y1 implies x / y = x1 / y1 )
the carrier of H c= the carrier of Q by Def30;
then reconsider x1y1 = x1 / y1 as Element of Q ;
assume A1: ( x = x1 & y = y1 ) ; :: thesis: x / y = x1 / y1
then x1y1 * y = (x1 / y1) * y1 by Th36
.= x by A1 ;
hence x / y = x1 / y1 ; :: thesis: verum