set Q = S -sequents ;
set F = Funcs ((bool (S -sequents)),(bool (S -sequents)));
reconsider RR = union D as Relation of (bool (S -sequents)) by FOMODEL0:19;
deffunc H₁( Element of bool (S -sequents)) -> Element of bool (S -sequents) = union (RR .: {$1});
consider f being Function of (bool (S -sequents)),(bool (S -sequents)) such that
A1: for x being Element of bool (S -sequents) holds f . x = H₁(x) from FUNCT_2:sch 4();
reconsider ff = f as Element of Funcs ((bool (S -sequents)),(bool (S -sequents))) by FUNCT_2:8;
take ff ; :: thesis: for Seqs being Element of bool (S -sequents) holds ff . Seqs = union ((union D) .: {Seqs})
thus for Seqs being Element of bool (S -sequents) holds ff . Seqs = union ((union D) .: {Seqs}) by A1; :: thesis: verum