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 I being integer SortSymbol of S
for X being V3() countable 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 M being pure Element of the generators of G . (the_array_sort_of S)
for i, x being pure Element of the generators of G . I holds (@ M) . (@ i) <> x
let I be integer SortSymbol of S; :: thesis: for X being V3() countable 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 M being pure Element of the generators of G . (the_array_sort_of S)
for i, x being pure Element of the generators of G . I holds (@ M) . (@ i) <> x
let X be V3() countable 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 M being pure Element of the generators of G . (the_array_sort_of S)
for i, x being pure Element of the generators of G . I holds (@ M) . (@ i) <> x
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 M being pure Element of the generators of G . (the_array_sort_of S)
for i, x being pure Element of the generators of G . I holds (@ M) . (@ i) <> x
let G be basic GeneratorSystem over S,X,T; :: thesis: for M being pure Element of the generators of G . (the_array_sort_of S)
for i, x being pure Element of the generators of G . I holds (@ M) . (@ i) <> x
let M be pure Element of the generators of G . (the_array_sort_of S); :: thesis: for i, x being pure Element of the generators of G . I holds (@ M) . (@ i) <> x
let i, x be pure Element of the generators of G . I; :: thesis: (@ M) . (@ i) <> x
set C = the bool-correct 4,1 integer 11,1,1 -array image of T;
set ST = the bool-correct 4,1 integer 11,1,1 -array image of T -States the generators of G;
assume A1: (@ M) . (@ i) = x ; :: thesis: contradiction
set q = the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T;
set g = (( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) +* (I,i,0);
set a = the_array_sort_of S;
consider h being ManySortedFunction of T, the bool-correct 4,1 integer 11,1,1 -array image of T such that
A2: ( h is_homomorphism T, the bool-correct 4,1 integer 11,1,1 -array image of T & h || (FreeGen T) = (( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) +* (I,i,0) ) by MSAFREE4:def 12;
reconsider s = h || the generators of G as Element of the bool-correct 4,1 integer 11,1,1 -array image of T -States the generators of G by A2, AOFA_A00:def 19;
A3: the_array_sort_of S <> I by Th73;
A4: ( (@ M) value_at ( the bool-correct 4,1 integer 11,1,1 -array image of T,s) = (s . (the_array_sort_of S)) . M & (@ i) value_at ( the bool-correct 4,1 integer 11,1,1 -array image of T,s) = (s . I) . i & ((@ M) . (@ i)) value_at ( the bool-correct 4,1 integer 11,1,1 -array image of T,s) = ((@ M) value_at ( the bool-correct 4,1 integer 11,1,1 -array image of T,s)) . ((@ i) value_at ( the bool-correct 4,1 integer 11,1,1 -array image of T,s)) ) by Th79, Th61;
A5: ( i in (FreeGen T) . I & x in (FreeGen T) . I & M in (FreeGen T) . (the_array_sort_of S) ) by Def4;
A6: ( dom ((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) . I) = (FreeGen T) . I & 0 in INT & INT = the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T . I ) by INT_1:def 2, AOFA_A00:55, FUNCT_2:def 1;
((h . I) | ( the generators of G . I)) . i = (h . I) . i by FUNCT_1:49;
then A7: (s . I) . i = (h . I) . i by MSAFREE:def 1
.= ((h . I) | ((FreeGen T) . I)) . i by Def4, FUNCT_1:49
.= (((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) +* (I,i,0)) . I) . i by A2, MSAFREE:def 1
.= (((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) . I) +* (i,0)) . i by A5, A6, AOFA_A00:def 2
.= 0 by Def4, A6, FUNCT_7:31 ;
reconsider 01 = 1 as Element of INT by INT_1:def 2;
A8: ( <%01%> in INT ^omega & the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T . (the_array_sort_of S) = INT ^omega & dom (( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) . (the_array_sort_of S)) = (FreeGen T) . (the_array_sort_of S) & dom ( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T . I) = (FreeGen T) . I & dom ((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) . (the_array_sort_of S)) = (FreeGen T) . (the_array_sort_of S) ) by Th74, AFINSQ_1:def 7, FUNCT_2:def 1;
A9: (s . (the_array_sort_of S)) . M = ((h . (the_array_sort_of S)) | ( the generators of G . (the_array_sort_of S))) . M by MSAFREE:def 1
.= (h . (the_array_sort_of S)) . M by FUNCT_1:49
.= ((h . (the_array_sort_of S)) | ((FreeGen T) . (the_array_sort_of S))) . M by Def4, FUNCT_1:49
.= (((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) +* (I,i,0)) . (the_array_sort_of S)) . M by A2, MSAFREE:def 1
.= ((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) . (the_array_sort_of S)) . M by A5, A6, A3, AOFA_A00:def 2
.= ((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) . (the_array_sort_of S)) +* (M,<%1%>)) . M by A8, A5, AOFA_A00:def 2
.= <%1%> by Def4, A8, FUNCT_7:31 ;
0 < len ((s . (the_array_sort_of S)) . M) by A9, AFINSQ_1:34;
then 0 in dom ((s . (the_array_sort_of S)) . M) by AFINSQ_1:86;
then (@ x) value_at ( the bool-correct 4,1 integer 11,1,1 -array image of T,s) = ((s . (the_array_sort_of S)) . M) . ((s . I) . i) by A1, A4, Th74, A7;
then A10: (s . I) . x = <%1%> . ((s . I) . i) by A9, Th61
.= 1 by A7 ;
(s . I) . x = ((h . I) | ( the generators of G . I)) . x by MSAFREE:def 1
.= (h . I) . x by FUNCT_1:49
.= ((h . I) | ((FreeGen T) . I)) . x by Def4, FUNCT_1:49
.= (((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) +* (I,i,0)) . I) . x by A2, MSAFREE:def 1
.= (((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) . I) +* (i,0)) . x by A5, A6, AOFA_A00:def 2
.= ((( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) +* ((the_array_sort_of S),M,<%1%>)) . I) . x by A7, A10, FUNCT_7:32
.= (( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T +* (I,x,0)) . I) . x by A3, A5, A8, AOFA_A00:def 2
.= (( the ManySortedFunction of FreeGen T, the Sorts of the bool-correct 4,1 integer 11,1,1 -array image of T . I) +* (x,0)) . x by A5, A6, AOFA_A00:def 2
.= 0 by Def4, A8, FUNCT_7:31 ;
hence contradiction by A10; :: thesis: verum