let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; for X being V3() ManySortedSet of the carrier of S
for T being non-empty b1,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for C being bool-correct 4,1 integer 11,1,1 -array 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
for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
let X be V3() ManySortedSet of the carrier of S; for T being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for C being bool-correct 4,1 integer 11,1,1 -array 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
for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; for C being bool-correct 4,1 integer 11,1,1 -array 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
for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
let C be bool-correct 4,1 integer 11,1,1 -array 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
for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
let G be basic GeneratorSystem over S,X,T; for I being integer SortSymbol of S
for s being Element of C -States the generators of G
for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
let I be integer SortSymbol of S; for s being Element of C -States the generators of G
for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
let s be Element of C -States the generators of G; for t1, t2 being Element of T,I holds (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
let t1, t2 be Element of T,I; (init.array (t1,t2)) value_at (C,s) = init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
set o = In (( the connectives of S . 14), the carrier' of 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:
t2 value_at (C,s) = (f . I) . t2
by A1, Th29;
A3:
(init.array (t1,t2)) value_at (C,s) = (f . (the_array_sort_of S)) . (init.array (t1,t2))
by A1, Th29;
A4:
( the_arity_of (In (( the connectives of S . 14), the carrier' of S)) = <*I,I*> & the_result_sort_of (In (( the connectives of S . 14), the carrier' of S)) = the_array_sort_of S )
by Th78;
then
Args ((In (( the connectives of S . 14), the carrier' of S)),T) = product <*( the Sorts of T . I),( the Sorts of T . I)*>
by Th23;
then reconsider p = <*t1,t2*> as Element of Args ((In (( the connectives of S . 14), the carrier' of S)),T) by FINSEQ_3:124;
thus (init.array (t1,t2)) value_at (C,s) =
(Den ((In (( the connectives of S . 14), the carrier' of S)),C)) . (f # p)
by A1, A3, A4
.=
(Den ((In (( the connectives of S . 14), the carrier' of S)),C)) . <*((f . I) . t1),((f . I) . t2)*>
by A4, Th26
.=
init.array ((t1 value_at (C,s)),(t2 value_at (C,s)))
by A1, A2, Th29
; verum