let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being non-empty b₁,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 t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)
let X be non-empty ManySortedSet of the carrier of S; :: thesis: 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 t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)
let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; :: thesis: 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 t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)
let C be bool-correct 4,1 integer 11,1,1 -array 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
for t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)
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
for t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)
let I be integer SortSymbol of S; :: thesis: for s being Element of C -States the generators of G
for t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)
let s be Element of C -States the generators of G; :: thesis: for t being Element of T,(the_array_sort_of S) holds (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)
let t be Element of T,(the_array_sort_of S); :: thesis: (length (t,I)) value_at (C,s) = length ((t value_at (C,s)),I)
set o = In (( the connectives of S . 13), 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: (length (t,I)) value_at (C,s) = (f . I) . (length (t,I)) by A1, Th29;
A3: ( the_arity_of (In (( the connectives of S . 13), the carrier' of S)) = <*(the_array_sort_of S)*> & the_result_sort_of (In (( the connectives of S . 13), the carrier' of S)) = I ) by Th77;
then Args ((In (( the connectives of S . 13), the carrier' of S)),T) = product <*( the Sorts of T . (the_array_sort_of S))*> by Th22;
then reconsider p = <*t*> as Element of Args ((In (( the connectives of S . 13), the carrier' of S)),T) by FINSEQ_3:123;
thus (length (t,I)) value_at (C,s) = (Den ((In (( the connectives of S . 13), the carrier' of S)),C)) . (f # p) by A1, A2, A3
.= (Den ((In (( the connectives of S . 13), the carrier' of S)),C)) . <*((f . (the_array_sort_of S)) . t)*> by A3, Th25
.= length ((t value_at (C,s)),I) by A1, Th29 ; :: thesis: verum