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 G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G holds (\true T) value_at (C,s) = TRUE
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 G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G holds (\true T) value_at (C,s) = TRUE
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 G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G holds (\true T) value_at (C,s) = TRUE
let C be bool-correct 4,1 integer image of T; for G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G holds (\true T) value_at (C,s) = TRUE
let G be basic GeneratorSystem over S,X,T; for s being Element of C -States the generators of G holds (\true T) value_at (C,s) = TRUE
let s be Element of C -States the generators of G; (\true T) value_at (C,s) = TRUE
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 & (\true T) value_at (C,s) = (f . the bool-sort of S) . (\true T) )
by A2, AOFA_A00:def 21;
set o = In (( the connectives of S . 1), the carrier' of S);
A4:
( 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 A4, MSUALG_3:6;
then A5:
p = f # p
;
(f . the bool-sort of S) . (\true T) =
\true C
by A5, A3, A4
.=
TRUE
by AOFA_A00:def 32
;
hence
(\true T) value_at (C,s) = TRUE
by A3; verum