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 u being ManySortedFunction of FreeGen T, the Sorts of C
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,u) = (t1 value_at (C,u)) \and (t2 value_at (C,u))
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 u being ManySortedFunction of FreeGen T, the Sorts of C
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,u) = (t1 value_at (C,u)) \and (t2 value_at (C,u))
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 u being ManySortedFunction of FreeGen T, the Sorts of C
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,u) = (t1 value_at (C,u)) \and (t2 value_at (C,u))
let C be bool-correct 4,1 integer image of T; for u being ManySortedFunction of FreeGen T, the Sorts of C
for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,u) = (t1 value_at (C,u)) \and (t2 value_at (C,u))
let u be ManySortedFunction of FreeGen T, the Sorts of C; for t1, t2 being Element of T, the bool-sort of S holds (t1 \and t2) value_at (C,u) = (t1 value_at (C,u)) \and (t2 value_at (C,u))
let t1, t2 be Element of T, the bool-sort of S; (t1 \and t2) value_at (C,u) = (t1 value_at (C,u)) \and (t2 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:
t1 value_at (C,u) = (f . the bool-sort of S) . t1
by A1, Th28;
A3:
(t1 \and t2) value_at (C,u) = (f . the bool-sort of S) . (t1 \and t2)
by A1, Th28;
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,u) =
(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,u)) \and (t2 value_at (C,u))
by A2, A1, Th28
; verum