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};
B0: dom R = bool (S -sequents) by FUNCT_2:def 1
.= dom (OneStep {R}) by FUNCT_2:def 1 ;

now

let x be set ; :: thesis: ( x in dom R implies R . x = (OneStep {R}) . x )
assume C1: x in dom R ; :: thesis: R . x = (OneStep {R}) . x
thus R . x = union {(R . x)} by ZFMISC_1:25
.= union (Im (R,x)) by C1, FUNCT_1:59
.= union ((union {R}) .: {x}) by ZFMISC_1:25
.= (OneStep {R}) . x by Def1Step, C1 ; :: thesis: verum

end;

hence R = OneStep {R} by B0, FUNCT_1:2; :: thesis: verum