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 i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for s being Element of C -States the generators of G
for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
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 i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for s being Element of C -States the generators of G
for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
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 i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for s being Element of C -States the generators of G
for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
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 i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for s being Element of C -States the generators of G
for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
let G be basic GeneratorSystem over S,X,T; for I being integer SortSymbol of S
for i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for s being Element of C -States the generators of G
for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
let I be integer SortSymbol of S; for i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for s being Element of C -States the generators of G
for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
let i be pure Element of the generators of G . I; for M being pure Element of the generators of G . (the_array_sort_of S)
for s being Element of C -States the generators of G
for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
let M be pure Element of the generators of G . (the_array_sort_of S); for s being Element of C -States the generators of G
for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
let s be Element of C -States the generators of G; for j being Integer st j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) holds
((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
let j be Integer; ( j in dom ((s . (the_array_sort_of S)) . M) & (@ M) . (@ i) in the generators of G . I & j = (@ i) value_at (C,s) implies ((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i)) )
assume A1:
j in dom ((s . (the_array_sort_of S)) . M)
; ( not (@ M) . (@ i) in the generators of G . I or not j = (@ i) value_at (C,s) or ((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i)) )
assume A2:
(@ M) . (@ i) in the generators of G . I
; ( not j = (@ i) value_at (C,s) or ((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i)) )
assume A3:
j = (@ i) value_at (C,s)
; ((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) = (s . I) . ((@ M) . (@ i))
reconsider s1 = s as ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
consider h being ManySortedFunction of T,C such that
A4:
( h is_homomorphism T,C & s1 = h || the generators of G )
by AOFA_A00:def 19;
(s . (the_array_sort_of S)) . M = (@ M) value_at (C,s)
by Th61;
hence ((s . (the_array_sort_of S)) . M) . ((@ i) value_at (C,s)) =
((@ M) value_at (C,s)) . ((@ i) value_at (C,s))
by A1, A3, Th74
.=
((@ M) . (@ i)) value_at (C,s)
by Th79
.=
(h . I) . ((@ M) . (@ i))
by A4, Th29
.=
((h . I) | ( the generators of G . I)) . ((@ M) . (@ i))
by A2, FUNCT_1:49
.=
(s . I) . ((@ M) . (@ i))
by A4, MSAFREE:def 1
;
verum