let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being V3() ManySortedSet of the carrier of S
for T being b₁,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
for t being Element of T, the bool-sort of S holds (\not t) value_at (C,u) = \not (t value_at (C,u))
let X be V3() ManySortedSet of the carrier of S; :: thesis: 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
for t being Element of T, the bool-sort of S holds (\not t) value_at (C,u) = \not (t value_at (C,u))
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: for C being bool-correct 4,1 integer image of T
for u being ManySortedFunction of FreeGen T, the Sorts of C
for t being Element of T, the bool-sort of S holds (\not t) value_at (C,u) = \not (t value_at (C,u))
let C be bool-correct 4,1 integer image of T; :: thesis: for u being ManySortedFunction of FreeGen T, the Sorts of C
for t being Element of T, the bool-sort of S holds (\not t) value_at (C,u) = \not (t value_at (C,u))
let u be ManySortedFunction of FreeGen T, the Sorts of C; :: thesis: for t being Element of T, the bool-sort of S holds (\not t) value_at (C,u) = \not (t value_at (C,u))
let t be Element of T, the bool-sort of S; :: thesis: (\not t) value_at (C,u) = \not (t value_at (C,u))
consider f being ManySortedFunction of T,C such that
A1: ( f is_homomorphism T,C & u = f || (FreeGen T) ) by MSAFREE4:46;
A2: (\not t) value_at (C,u) = (f . the bool-sort of S) . (\not t) by A1, Th28;
set o = In (( the connectives of S . 2), the carrier' of S);
A3: ( the_arity_of (In (( the connectives of S . 2), the carrier' of S)) = <* the bool-sort of S*> & the_result_sort_of (In (( the connectives of S . 2), the carrier' of S)) = the bool-sort of S ) by Th12;
then Args ((In (( the connectives of S . 2), the carrier' of S)),T) = product <*( the Sorts of T . the bool-sort of S)*> by Th22;
then reconsider p = <*t*> as Element of Args ((In (( the connectives of S . 2), the carrier' of S)),T) by FINSEQ_3:123;
thus (\not t) value_at (C,u) = (Den ((In (( the connectives of S . 2), the carrier' of S)),C)) . (f # p) by A1, A2, A3
.= (Den ((In (( the connectives of S . 2), the carrier' of S)),C)) . <*((f . the bool-sort of S) . t)*> by A3, Th25
.= \not (t value_at (C,u)) by A1, Th28 ; :: thesis: verum