let f, g be Function of (bool the carrier of R),(bool the carrier of R); :: thesis: ( ( for X being Subset of R holds f . X = UAp X ) & ( for X being Subset of R holds g . X = UAp X ) implies f = g )
assume that
A5: for X being Subset of R holds f . X = UAp X and
A6: for X being Subset of R holds g . X = UAp X ; :: thesis: f = g
let Y be Subset of R; :: according to FUNCT_2:def 8 :: thesis: f . Y = g . Y
thus f . Y = UAp Y by A5
.= g . Y by A6 ; :: thesis: verum