deffunc H₁( object ) -> set = { x where x is Element of S -sequents : [$1,x] in R } ;
A1: for inseqs being set holds H₁(inseqs) in bool (S -sequents)

proof

let inseqs be set ; :: thesis: H₁(inseqs) in bool (S -sequents)

now :: thesis: for x being object st x in H₁(inseqs) holds
x in S -sequents

let x be object ; :: thesis: ( x in H₁(inseqs) implies x in S -sequents )
assume x in H₁(inseqs) ; :: thesis: x in S -sequents
then consider seq being Element of S -sequents such that
A2: ( seq = x & [inseqs,seq] in R ) ;
thus x in S -sequents by A2; :: thesis: verum

end;

then H₁(inseqs) c= S -sequents by TARSKI:def 3;
hence H₁(inseqs) in bool (S -sequents) ; :: thesis: verum

end;

A3: for inseqs being object st inseqs in bool (S -sequents) holds
H₁(inseqs) in bool (S -sequents) by A1;
consider f being Function of (bool (S -sequents)),(bool (S -sequents)) such that
A4: for x being object st x in bool (S -sequents) holds
f . x = H₁(x) from FUNCT_2:sch 2(A3);
take f ; :: thesis: ( f is Rule of S & ( for inseqs being set st inseqs in bool (S -sequents) holds
f . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) )
thus ( f is Rule of S & ( for inseqs being set st inseqs in bool (S -sequents) holds
f . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) ) by A4, FUNCT_2:8; :: thesis: verum