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 s being Element of C -States the generators of G
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))
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 s being Element of C -States the generators of G
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))
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 s being Element of C -States the generators of G
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for s being Element of C -States the generators of G
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))
let G be basic GeneratorSystem over S,X,T; :: thesis: for s being Element of C -States the generators of G
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))
let s be Element of C -States the generators of G; :: thesis: for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))
let t1, t2 be Element of T, the bool-sort of S; :: thesis: (t1 \and t2) value_at (C,s) = (t1 value_at (C,s)) \and (t2 value_at (C,s))
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
A1: ( f is_homomorphism T,C & s = f || the generators of G ) by AOFA_A00:def 19;
A2: t1 value_at (C,s) = (f . the bool-sort of S) . t1 by A1, Th29;
A3: (t1 \and t2) value_at (C,s) = (f . the bool-sort of S) . (t1 \and t2) by A1, Th29;
set o = In (( the connectives of S . 3), the carrier' of S);
A4: ( the_arity_of (In (( the connectives of S . 3), the carrier' of S)) = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of (In (( the connectives of S . 3), the carrier' of S)) = the bool-sort of S ) by Th13;
then Args ((In (( the connectives of S . 3), the carrier' of S)),T) = product <*( the Sorts of T . the bool-sort of S),( the Sorts of T . the bool-sort of S)*> by Th23;
then reconsider p = <*t1,t2*> as Element of Args ((In (( the connectives of S . 3), the carrier' of S)),T) by FINSEQ_3:124;
thus (t1 \and t2) value_at (C,s) = (Den ((In (( the connectives of S . 3), the carrier' of S)),C)) . (f # p) by A1, A3, A4
.= (Den ((In (( the connectives of S . 3), the carrier' of S)),C)) . <*((f . the bool-sort of S) . t1),((f . the bool-sort of S) . t2)*> by A4, Th26
.= (t1 value_at (C,s)) \and (t2 value_at (C,s)) by A2, A1, Th29 ; :: thesis: verum