let S be non empty non void bool-correct 4,1 integer BoolSignature ; for X being V3() ManySortedSet of the carrier of S
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\false T) value_at (C,u) = FALSE
let X be V3() ManySortedSet of the carrier of S; for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\false T) value_at (C,u) = FALSE
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; for C being bool-correct 4,1 integer image of T
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\false T) value_at (C,u) = FALSE
let C be bool-correct 4,1 integer image of T; for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\false T) value_at (C,u) = FALSE
let u be ManySortedFunction of FreeGen T, the Sorts of C; (\false T) value_at (C,u) = FALSE
thus (\false T) value_at (C,u) =
\not ((\true T) value_at (C,u))
by Th47
.=
'not' ((\true T) value_at (C,u))
by AOFA_A00:def 32
.=
'not' TRUE
by Th46
.=
FALSE
; verum