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