let f, g be Function of (bool the carrier of A),(bool the carrier of A); :: thesis: ( ( for x being Subset of A holds f . x = x % I ) & ( for x being Subset of A holds g . x = x % I ) implies f = g )
assume that
A2: for X being Subset of A holds f . X = X % I and
A3: for X being Subset of A holds g . X = X % I ; :: thesis: f = g
for Y being Subset of A holds f . Y = g . Y
proof
let Y be Subset of A; :: thesis: f . Y = g . Y
f . Y = Y % I by A2
.= g . Y by A3 ;
hence f . Y = g . Y ; :: thesis: verum
end;
hence f = g ; :: thesis: verum