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

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