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
phi is V278()
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
phi is V278()
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 phi is V278() )
assume A1: for X being Subset of (Funcs (Q,Q)) holds phi . X = MltClos1 (H,X) ; :: thesis: phi is V278()
let a1, b1 be set ; :: according to COHSP_1:def 11 :: thesis: ( not a1 in dom phi or not b1 in dom phi or not a1 c= b1 or phi . a1 c= phi . b1 )
assume A2: ( a1 in dom phi & b1 in dom phi & a1 c= b1 ) ; :: thesis: phi . a1 c= phi . b1
thus phi . a1 c= phi . b1 :: thesis: verum
proof
reconsider a2 = a1, b2 = b1 as Subset of (Funcs (Q,Q)) by A2, FUNCT_2:def 1;
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in phi . a1 or f in phi . b1 )
assume f in phi . a1 ; :: thesis: f in phi . b1
then f in MltClos1 (H,a2) by A1;
then S2[Q,H,a2,f] by Def37;
then f in MltClos1 (H,b2) by A2, Def37;
hence f in phi . b1 by A1; :: thesis: verum
end;