let q, p be boolean-valued Function; :: thesis: ( dom q = dom p & ( for x being object st x in dom p holds
q . x = 'not' (p . x) ) implies ( dom p = dom q & ( for x being object st x in dom q holds
p . x = 'not' (q . x) ) ) )
assume that
A10: dom q = dom p and
A11: for x being object st x in dom p holds
q . x = 'not' (p . x) ; :: thesis: ( dom p = dom q & ( for x being object st x in dom q holds
p . x = 'not' (q . x) ) )
thus dom p = dom q by A10; :: thesis: for x being object st x in dom q holds
p . x = 'not' (q . x)
let x be object ; :: thesis: ( x in dom q implies p . x = 'not' (q . x) )
assume A12: x in dom q ; :: thesis: p . x = 'not' (q . x)
thus p . x = 'not' ('not' (p . x))
.= 'not' (q . x) by A10, A11, A12 ; :: thesis: verum