set Q = S -sequents ;
let IT1, IT2 be Rule of S; :: thesis: ( ( for inseqs being set st inseqs in bool (S -sequents) holds
IT1 . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) & ( for inseqs being set st inseqs in bool (S -sequents) holds
IT2 . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) implies IT1 = IT2 )
deffunc H₁( object ) -> set = { x where x is Element of S -sequents : [$1,x] in R } ;
assume A5: for inseqs being set st inseqs in bool (S -sequents) holds
IT1 . inseqs = H₁(inseqs) ; :: thesis: ( ex inseqs being set st
( inseqs in bool (S -sequents) & not IT2 . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) or IT1 = IT2 )
assume A6: for inseqs being set st inseqs in bool (S -sequents) holds
IT2 . inseqs = H₁(inseqs) ; :: thesis: IT1 = IT2
for x being object st x in bool (S -sequents) holds
IT1 . x = IT2 . x

proof

let x be object ; :: thesis: ( x in bool (S -sequents) implies IT1 . x = IT2 . x )
assume A7: x in bool (S -sequents) ; :: thesis: IT1 . x = IT2 . x
hence IT1 . x = H₁(x) by A5
.= IT2 . x by A6, A7 ;
:: thesis: verum

end;

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