let R1, R2 be Function; :: thesis: ( dom R1 = bool A & ( for X being set st X c= A holds
R1 . X = R .: X ) & dom R2 = bool A & ( for X being set st X c= A holds
R2 . X = R .: X ) implies R1 = R2 )
assume that
A4: dom R1 = bool A and
A5: for X being set st X c= A holds
R1 . X = R .: X and
A6: dom R2 = bool A and
A7: for X being set st X c= A holds
R2 . X = R .: X ; :: thesis: R1 = R2
for x being object st x in bool A holds
R1 . x = R2 . x

proof

let x be object ; :: thesis: ( x in bool A implies R1 . x = R2 . x )
assume A8: x in bool A ; :: thesis: R1 . x = R2 . x
reconsider xx = x as set by TARSKI:1;
R1 . x = R .: xx by A5, A8;
hence R1 . x = R2 . x by A7, A8; :: thesis: verum

end;

hence R1 = R2 by A4, A6, FUNCT_1:2; :: thesis: verum