let q1, q2 be boolean-valued Function; :: thesis: ( dom q1 = dom p & ( for x being object st x in dom p holds
q1 . x = 'not' (p . x) ) & dom q2 = dom p & ( for x being object st x in dom p holds
q2 . x = 'not' (p . x) ) implies q1 = q2 )
assume that
A5: dom q1 = dom p and
A6: for x being object st x in dom p holds
q1 . x = 'not' (p . x) and
A7: dom q2 = dom p and
A8: for x being object st x in dom p holds
q2 . x = 'not' (p . x) ; :: thesis: q1 = q2
for x being object st x in dom p holds
q1 . x = q2 . x

proof

let x be object ; :: thesis: ( x in dom p implies q1 . x = q2 . x )
assume A9: x in dom p ; :: thesis: q1 . x = q2 . x
then q1 . x = 'not' (p . x) by A6;
hence q1 . x = q2 . x by A8, A9; :: thesis: verum

end;

hence q1 = q2 by A5, A7; :: thesis: verum