let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty 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 holds (\true T) value_at (C,u) = TRUE
let X be non-empty 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 holds (\true T) value_at (C,u) = TRUE
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 holds (\true T) value_at (C,u) = TRUE
let C be bool-correct 4,1 integer image of T; :: thesis: for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\true T) value_at (C,u) = TRUE
let u be ManySortedFunction of FreeGen T, the Sorts of C; :: thesis: (\true T) value_at (C,u) = TRUE
consider f being ManySortedFunction of T,C such that
A1: ( f is_homomorphism T,C & u = f || (FreeGen T) ) by MSAFREE4:46;
FreeGen T is_transformable_to the Sorts of C by MSAFREE4:21;
then doms u = FreeGen T by MSSUBFAM:17;
then consider f being ManySortedFunction of T,C, Q being GeneratorSet of T such that
A2: ( f is_homomorphism T,C & Q = doms u & u = f || Q & (\true T) value_at (C,u) = (f . the bool-sort of S) . (\true T) ) by A1, AOFA_A00:def 21;
set o = In (( the connectives of S . 1), the carrier' of S);
A3: ( In (( the connectives of S . 1), the carrier' of S) = the connectives of S . 1 & the_arity_of (In (( the connectives of S . 1), the carrier' of S)) = {} & the_result_sort_of (In (( the connectives of S . 1), the carrier' of S)) = the bool-sort of S ) by Th11;
then Args ((In (( the connectives of S . 1), the carrier' of S)),T) = {{}} by Th21;
then reconsider p = {} as Element of Args ((In (( the connectives of S . 1), the carrier' of S)),T) by TARSKI:def 1;
( dom (f # p) = {} & dom p = {} ) by A3, MSUALG_3:6;
then A4: p = f # p ;
(f . the bool-sort of S) . (\true T) = \true C by A4, A2, A3
.= TRUE by AOFA_A00:def 32 ;
hence (\true T) value_at (C,u) = TRUE by A2; :: thesis: verum