let Q be multLoop; :: thesis: for H being Subset of Q
for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Mlt H
let H be Subset of Q; :: thesis: for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Mlt H
let u be Element of Q; :: thesis: ( u in H implies (curry' the multF of Q) . u in Mlt H )
H left-right-mult-closed Mlt H by Def38;
hence ( u in H implies (curry' the multF of Q) . u in Mlt H ) ; :: thesis: verum