let s1, s2 be Function; :: thesis: ( dom s1 = (dom p) /\ (dom q) & ( for x being set st x in dom s1 holds
s1 . x = (p . x) 'xor' (q . x) ) & dom s2 = (dom p) /\ (dom q) & ( for x being set st x in dom s2 holds
s2 . x = (p . x) 'xor' (q . x) ) implies s1 = s2 )
assume that
A11: dom s1 = (dom p) /\ (dom q) and
A12: for x being set st x in dom s1 holds
s1 . x = (p . x) 'xor' (q . x) and
A13: dom s2 = (dom p) /\ (dom q) and
A14: for x being set st x in dom s2 holds
s2 . x = (p . x) 'xor' (q . x) ; :: thesis: s1 = s2
for x being set st x in dom s1 holds
s1 . x = s2 . x

proof

let x be set ; :: thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume x in dom s1 ; :: thesis: s1 . x = s2 . x
then ( s1 . x = (p . x) 'xor' (q . x) & s2 . x = (p . x) 'xor' (q . x) ) by A11, A12, A13, A14;
hence s1 . x = s2 . x ; :: thesis: verum

end;

hence s1 = s2 by A11, A13, FUNCT_1:9; :: thesis: verum