let X, y be set ; :: thesis: for S being Language
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) )
let S be Language; :: thesis: for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) )
set Q = S -sequents ;
let R be Relation of (bool (S -sequents)),(S -sequents); :: thesis: ( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) )
reconsider F = FuncRule R as Function of (bool (S -sequents)),(bool (S -sequents)) ;

per cases ( not X in bool (S -sequents) or X in bool (S -sequents) ) ;

suppose A1: not X in bool (S -sequents) ; :: thesis: ( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) )

not X in dom F by A1;
hence ( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) ) by A1, ZFMISC_1:87, FUNCT_1:def 2; :: thesis: verum

end;

suppose X in bool (S -sequents) ; :: thesis: ( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) )

then reconsider Seqts = X as Element of bool (S -sequents) ;
set SQ = Seqts;
( y in (FuncRule R) . Seqts iff ( y in S -sequents & [Seqts,y] in R ) ) by Lm29;
hence ( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) ) ; :: thesis: verum

end;

end;