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 V3() 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 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; :: 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 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; :: 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 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( 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 ; :: thesis: ( 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) ; :: thesis: ((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 ;
:: thesis: verum