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;