set Q = S -sequents ;
set F = Funcs ((bool (S -sequents)),(bool (S -sequents)));
let IT1, IT2 be Rule of S; :: thesis: ( ( for Seqs being Element of bool (S -sequents) holds IT1 . Seqs = union ((union D) .: {Seqs}) ) & ( for Seqs being Element of bool (S -sequents) holds IT2 . Seqs = union ((union D) .: {Seqs}) ) implies IT1 = IT2 )
reconsider IT11 = IT1, IT22 = IT2 as Function of (bool (S -sequents)),(bool (S -sequents)) ;
deffunc H₁( set ) -> set = union ((union D) .: {$1});
assume A2: for Seqs being Element of bool (S -sequents) holds IT1 . Seqs = H₁(Seqs) ; :: thesis: ( ex Seqs being Element of bool (S -sequents) st not IT2 . Seqs = union ((union D) .: {Seqs}) or IT1 = IT2 )
assume A3: for Seqs being Element of bool (S -sequents) holds IT2 . Seqs = H₁(Seqs) ; :: thesis: IT1 = IT2

now :: thesis: for x being Element of bool (S -sequents) holds IT11 . x = IT22 . x

let x be Element of bool (S -sequents); :: thesis: IT11 . x = IT22 . x
thus IT11 . x = H₁(x) by A2
.= IT22 . x by A3 ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum