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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for M being pure Element of the generators of G . (the_array_sort_of S) st G is integer-array holds
for t being Element of T,I holds (@ M) . t in the generators of G . 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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for M being pure Element of the generators of G . (the_array_sort_of S) st G is integer-array holds
for t being Element of T,I holds (@ M) . t in the generators of G . 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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for M being pure Element of the generators of G . (the_array_sort_of S) st G is integer-array holds
for t being Element of T,I holds (@ M) . t in the generators of G . I
let G be basic GeneratorSystem over S,X,T; :: thesis: for I being integer SortSymbol of S
for M being pure Element of the generators of G . (the_array_sort_of S) st G is integer-array holds
for t being Element of T,I holds (@ M) . t in the generators of G . I
let I be integer SortSymbol of S; :: thesis: for M being pure Element of the generators of G . (the_array_sort_of S) st G is integer-array holds
for t being Element of T,I holds (@ M) . t in the generators of G . I
let M be pure Element of the generators of G . (the_array_sort_of S); :: thesis: ( G is integer-array implies for t being Element of T,I holds (@ M) . t in the generators of G . I )
assume A1: G is integer-array ; :: thesis: for t being Element of T,I holds (@ M) . t in the generators of G . I
let t be Element of T,I; :: thesis: (@ M) . t in the generators of G . I
A2: (@ M) . t in { ((@ N) . q) where N is pure Element of the generators of G . (the_array_sort_of S), q is Element of T,I : verum } ;
{ ((@ N) . q) where N is pure Element of the generators of G . (the_array_sort_of S), q is Element of T,I : verum } c= the generators of G . I by A1;
hence (@ M) . t in the generators of G . I by A2; :: thesis: verum