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
x1 * y1 = ( the multF of Q || the carrier of H) . (x1,y1) by Def30
.= x * y by A1, RING_3:1 ;
hence x * y = x1 * y1 ; :: thesis: verum