let S be Language; :: thesis: for R being Rule of S holds R = OneStep {R}
let R be Rule of S; :: thesis: R = OneStep {R}
set IT = OneStep {R};
A1: dom R = bool (S -sequents) by FUNCT_2:def 1
.= dom (OneStep {R}) by FUNCT_2:def 1 ;
now :: thesis: for x being object st x in dom R holds
R . x = (OneStep {R}) . x
let x be object ; :: thesis: ( x in dom R implies R . x = (OneStep {R}) . x )
assume A2: x in dom R ; :: thesis: R . x = (OneStep {R}) . x
thus R . x = union {(R . x)}
.= union (Im (R,x)) by FUNCT_1:59, A2
.= union ((union {R}) .: {x})
.= (OneStep {R}) . x by Def5, A2 ; :: thesis: verum
end;
hence R = OneStep {R} by A1, FUNCT_1:2; :: thesis: verum