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 = LAp X ) & ( for X being Subset of R holds g . X = LAp X ) implies f = g )
assume that
A2: for X being Subset of R holds f . X = LAp X and
A3: for X being Subset of R holds g . X = LAp X ; :: thesis: f = g
let Y be Subset of R; :: according to FUNCT_2:def 8 :: thesis: f . Y = g . Y
thus f . Y = LAp Y by A2
.= g . Y by A3 ; :: thesis: verum