let f1, f2 be Function; :: thesis: ( dom f1 = X & ( for x being object st x in X holds
( ( x in A implies f1 . x = 1 ) & ( not x in A implies f1 . x = 0 ) ) ) & dom f2 = X & ( for x being object st x in X holds
( ( x in A implies f2 . x = 1 ) & ( not x in A implies f2 . x = 0 ) ) ) implies f1 = f2 )
assume that
A3: dom f1 = X and
A4: for x being object st x in X holds
( ( x in A implies f1 . x = 1 ) & ( not x in A implies f1 . x = 0 ) ) and
A5: dom f2 = X and
A6: for x being object st x in X holds
( ( x in A implies f2 . x = 1 ) & ( not x in A implies f2 . x = 0 ) ) ; :: thesis: f1 = f2
for x being object st x in X holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in X implies f1 . x = f2 . x )
assume A7: x in X ; :: thesis: f1 . x = f2 . x
then A8: ( not x in A implies ( f1 . x = 0 & f2 . x = 0 ) ) by A4, A6;
( x in A implies ( f1 . x = 1 & f2 . x = 1 ) ) by A4, A6, A7;
hence f1 . x = f2 . x by A8; :: thesis: verum

end;

hence f1 = f2 by A3, A5; :: thesis: verum