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 )
assume A1: ( x = x1 & y = y1 ) ; :: thesis: x \ y = x1 \ y1
the carrier of H c= the carrier of Q by Def30;
then reconsider x1y1 = x1 \ y1 as Element of Q ;
x * x1y1 = x1 * (x1 \ y1) by Th36, A1
.= y by A1 ;
hence x \ y = x1 \ y1 ; :: thesis: verum