for G, H being Function of S,(bool X) st ( for x being set st x in S holds
G . x = F_LABEL (x,X) ) & ( for x being set st x in S holds
H . x = F_LABEL (x,X) ) holds
G = H

proof

let G, H be Function of S,(bool X); :: thesis: ( ( for x being set st x in S holds
G . x = F_LABEL (x,X) ) & ( for x being set st x in S holds
H . x = F_LABEL (x,X) ) implies G = H )
assume that
A3: for x being set st x in S holds
G . x = F_LABEL (x,X) and
A4: for x being set st x in S holds
H . x = F_LABEL (x,X) ; :: thesis: G = H
for x being set st x in S holds
G . x = H . x

proof

let x be set ; :: 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

end;

hence for b₁, b₂ being Function of S,(bool X) st ( for x being set st x in S holds
b₁ . x = F_LABEL (x,X) ) & ( for x being set st x in S holds
b₂ . x = F_LABEL (x,X) ) holds
b₁ = b₂ ; :: thesis: verum