let F, G be Element of Funcs (D,(CQC-WFF A)); :: thesis: ( ( for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
F . a = 'not' p ) & ( for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
G . a = 'not' p ) implies F = G )
assume A3: for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
F . a = 'not' p ; :: thesis: ( ex a being Element of D ex p being Element of CQC-WFF A st
( p = f . a & not G . a = 'not' p ) or F = G )
assume A4: for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
G . a = 'not' p ; :: thesis: F = G
for a being Element of D holds F . a = G . a
proof
let a be Element of D; :: thesis: F . a = G . a
consider p being Element of CQC-WFF A such that
A5: p = f . a ;
thus F . a = 'not' p by A3, A5
.= G . a by A4, A5 ; :: thesis: verum
end;
hence F = G by FUNCT_2:63; :: thesis: verum