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 )
assume A1: u in H ; :: thesis: (curry the multF of Q) . u in Mlt H
H left-right-mult-closed Mlt H by Def38;
hence (curry the multF of Q) . u in Mlt H by A1; :: thesis: verum