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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for s being Element of C -States the generators of G holds (\0 (T,I)) value_at (C,s) = 0
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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for s being Element of C -States the generators of G holds (\0 (T,I)) value_at (C,s) = 0
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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for s being Element of C -States the generators of G holds (\0 (T,I)) value_at (C,s) = 0
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for s being Element of C -States the generators of G holds (\0 (T,I)) value_at (C,s) = 0
let G be basic GeneratorSystem over S,X,T; :: thesis: for I being integer SortSymbol of S
for s being Element of C -States the generators of G holds (\0 (T,I)) value_at (C,s) = 0
let I be integer SortSymbol of S; :: thesis: for s being Element of C -States the generators of G holds (\0 (T,I)) value_at (C,s) = 0
let s be Element of C -States the generators of G; :: thesis: (\0 (T,I)) value_at (C,s) = 0
A1: s is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
then consider f being ManySortedFunction of T,C such that
A2: ( f is_homomorphism T,C & s = f || the generators of G ) by AOFA_A00:def 19;
the generators of G is_transformable_to the Sorts of C by MSAFREE4:21;
then doms s = the generators of G by A1, MSSUBFAM:17;
then consider f being ManySortedFunction of T,C, Q being GeneratorSet of T such that
A3: ( f is_homomorphism T,C & Q = doms s & s = f || Q & (\0 (T,I)) value_at (C,s) = (f . I) . (\0 (T,I)) ) by A2, AOFA_A00:def 21;
set o = In (( the connectives of S . 4), the carrier' of S);
A4: ( the_arity_of (In (( the connectives of S . 4), the carrier' of S)) = {} & the_result_sort_of (In (( the connectives of S . 4), the carrier' of S)) = I ) by Th14;
then Args ((In (( the connectives of S . 4), the carrier' of S)),T) = {{}} by Th21;
then reconsider p = {} as Element of Args ((In (( the connectives of S . 4), the carrier' of S)),T) by TARSKI:def 1;
( dom (f # p) = {} & dom p = {} ) by A4, MSUALG_3:6;
then A5: p = f # p ;
(f . I) . (\0 (T,I)) = \0 (C,I) by A5, A3, A4
.= 0 by AOFA_A00:55 ;
hence (\0 (T,I)) value_at (C,s) = 0 by A3; :: thesis: verum