let Q be multLoop; :: thesis: for H being Subset of Q
for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds
for Y being Subset of (Funcs (Q,Q)) st phi . Y c= Y holds
( ( for u being Element of Q st u in H holds
(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Y ) )
let H be Subset of Q; :: thesis: for phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) st ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) holds
for Y being Subset of (Funcs (Q,Q)) st phi . Y c= Y holds
( ( for u being Element of Q st u in H holds
(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Y ) )
let phi be Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))); :: thesis: ( ( for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ) implies for Y being Subset of (Funcs (Q,Q)) st phi . Y c= Y holds
( ( for u being Element of Q st u in H holds
(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Y ) ) )
assume A1: for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ; :: thesis: for Y being Subset of (Funcs (Q,Q)) st phi . Y c= Y holds
( ( for u being Element of Q st u in H holds
(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Y ) )
let Y be Subset of (Funcs (Q,Q)); :: thesis: ( phi . Y c= Y implies ( ( for u being Element of Q st u in H holds
(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Y ) ) )
assume phi . Y c= Y ; :: thesis: ( ( for u being Element of Q st u in H holds
(curry the multF of Q) . u in Y ) & ( for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Y ) )
then A2: MltClos1 (H,Y) c= Y by A1;
thus for u being Element of Q st u in H holds
(curry the multF of Q) . u in Y :: thesis: for u being Element of Q st u in H holds
(curry' the multF of Q) . u in Y

proof

let u be Element of Q; :: thesis: ( u in H implies (curry the multF of Q) . u in Y )
assume u in H ; :: thesis: (curry the multF of Q) . u in Y
then (curry the multF of Q) . u in MltClos1 (H,Y) by Def37;
hence (curry the multF of Q) . u in Y by A2; :: thesis: verum

end;

let u be Element of Q; :: thesis: ( u in H implies (curry' the multF of Q) . u in Y )
assume u in H ; :: thesis: (curry' the multF of Q) . u in Y
then (curry' the multF of Q) . u in MltClos1 (H,Y) by Def37;
hence (curry' the multF of Q) . u in Y by A2; :: thesis: verum