let G, H be Function of S,(bool X); :: thesis: ( ( for x being object st x in S holds
G . x = F_LABEL (x,X) ) & ( for x being object st x in S holds
H . x = F_LABEL (x,X) ) implies G = H )
assume that
A3: for x being object st x in S holds
G . x = F_LABEL (x,X) and
A4: for x being object st x in S holds
H . x = F_LABEL (x,X) ; :: thesis: G = H
for x being object st x in S holds
G . x = H . x
proof
let x be object ; :: thesis: ( x in S implies G . x = H . x )
assume A5: x in S ; :: thesis: G . x = H . x
G . x = F_LABEL (x,X) by A3, A5
.= H . x by A4, A5 ;
hence G . x = H . x ; :: thesis: verum
end;
hence G = H by FUNCT_2:12; :: thesis: verum