let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args o,A st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o)
let A be non-empty MSAlgebra of S; :: thesis: for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args o,A st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o)
let o be OperSymbol of S; :: thesis: for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args o,A st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o)
let C1, C2 be MSCongruence of A; :: thesis: for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args o,A st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o)
let C be MSEquivalence-like ManySortedRelation of A; :: thesis: ( C = C1 "\/" C2 implies for x, y being Element of Args o,A st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o) )
assume A1:
C = C1 "\/" C2
; :: thesis: for x, y being Element of Args o,A st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o)
let x, y be Element of Args o,A; :: thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) implies [((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o) )
assume A2:
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n)
; :: thesis: [((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o)
defpred S1[ Element of NAT ] means for a1, a2, b1 being FinSequence st len a1 = $1 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . (a2 ^ b1))] in C . (the_result_sort_of o);
A3:
S1[ 0 ]
proof
let a1,
a2,
b1 be
FinSequence;
:: thesis: ( len a1 = 0 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) implies [((Den o,A) . x),((Den o,A) . (a2 ^ b1))] in C . (the_result_sort_of o) )
assume that A4:
len a1 = 0
and A5:
len a1 = len a2
and A6:
x = a1 ^ b1
and
for
n being
Nat st
n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n)
;
:: thesis: [((Den o,A) . x),((Den o,A) . (a2 ^ b1))] in C . (the_result_sort_of o)
A7:
(
a1 = {} &
a2 = {} )
by A4, A5;
A9: the
Sorts of
A . (the_result_sort_of o) =
the
Sorts of
A . (the ResultSort of S . o)
by MSUALG_1:def 7
.=
(the Sorts of A * the ResultSort of S) . o
by FUNCT_2:21
.=
Result o,
A
by MSUALG_1:def 10
;
field (C . (the_result_sort_of o)) = the
Sorts of
A . (the_result_sort_of o)
by ORDERS_1:97;
then
C . (the_result_sort_of o) is_reflexive_in the
Sorts of
A . (the_result_sort_of o)
by RELAT_2:def 9;
hence
[((Den o,A) . x),((Den o,A) . (a2 ^ b1))] in C . (the_result_sort_of o)
by A6, A7, A9, RELAT_2:def 1;
:: thesis: verum
end;
A10:
for l being Element of NAT st S1[l] holds
S1[l + 1]
proof
let l be
Element of
NAT ;
:: thesis: ( S1[l] implies S1[l + 1] )
assume A11:
for
a1,
a2,
b1 being
FinSequence st
len a1 = l &
len a1 = len a2 &
x = a1 ^ b1 & ( for
n being
Nat st
n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . (a2 ^ b1))] in C . (the_result_sort_of o)
;
:: thesis: S1[l + 1]
let a1,
a2,
b1 be
FinSequence;
:: thesis: ( len a1 = l + 1 & len a1 = len a2 & x = a1 ^ b1 & ( for n being Nat st n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n) ) implies [((Den o,A) . x),((Den o,A) . (a2 ^ b1))] in C . (the_result_sort_of o) )
assume that A12:
len a1 = l + 1
and A13:
len a1 = len a2
and A14:
x = a1 ^ b1
and A15:
for
n being
Nat st
n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n)
;
:: thesis: [((Den o,A) . x),((Den o,A) . (a2 ^ b1))] in C . (the_result_sort_of o)
set y =
a2 ^ b1;
a1 <> {}
by A12;
then consider q1 being
FinSequence,
x1 being
set such that A16:
a1 = q1 ^ <*x1*>
by FINSEQ_1:63;
a2 <> {}
by A12, A13;
then consider q2 being
FinSequence,
y1 being
set such that A17:
a2 = q2 ^ <*y1*>
by FINSEQ_1:63;
A18:
l + 1 =
(len q1) + (len <*x1*>)
by A12, A16, FINSEQ_1:35
.=
(len q1) + 1
by FINSEQ_1:57
;
then A19:
len q1 = l
by XCMPLX_1:2;
A20:
l + 1 =
(len q2) + (len <*y1*>)
by A12, A13, A17, FINSEQ_1:35
.=
(len q2) + 1
by FINSEQ_1:57
;
then A21:
len q1 = len q2
by A18, XCMPLX_1:2;
A22:
dom q1 =
Seg (len q1)
by FINSEQ_1:def 3
.=
dom q2
by A21, FINSEQ_1:def 3
;
A23:
for
n being
Element of
NAT st
n in dom q1 holds
[(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n)
proof
let n be
Element of
NAT ;
:: thesis: ( n in dom q1 implies [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n) )
assume A24:
n in dom q1
;
:: thesis: [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n)
then A25:
n in Seg (len q1)
by FINSEQ_1:def 3;
len q1 <= len a1
by A12, A18, NAT_1:11;
then
Seg (len q1) c= Seg (len a1)
by FINSEQ_1:7;
then
n in Seg (len a1)
by A25;
then A26:
n in dom a1
by FINSEQ_1:def 3;
then A27:
x . n =
a1 . n
by A14, FINSEQ_1:def 7
.=
q1 . n
by A16, A24, FINSEQ_1:def 7
;
dom a1 =
Seg (len a1)
by FINSEQ_1:def 3
.=
dom a2
by A13, FINSEQ_1:def 3
;
then (a2 ^ b1) . n =
a2 . n
by A26, FINSEQ_1:def 7
.=
q2 . n
by A17, A22, A24, FINSEQ_1:def 7
;
hence
[(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n)
by A15, A26, A27;
:: thesis: verum
end;
A28:
[((Den o,A) . x),((Den o,A) . ((q2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o)
proof
A29:
(q1 ^ <*x1*>) ^ b1 = q1 ^ (<*x1*> ^ b1)
by FINSEQ_1:45;
A30:
(q2 ^ <*x1*>) ^ b1 = q2 ^ (<*x1*> ^ b1)
by FINSEQ_1:45;
for
n being
Nat st
n in dom q1 holds
[(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n)
proof
let n be
Nat;
:: thesis: ( n in dom q1 implies [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n) )
assume A31:
n in dom q1
;
:: thesis: [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n)
then A32:
x . n = q1 . n
by A14, A16, A29, FINSEQ_1:def 7;
((q2 ^ <*x1*>) ^ b1) . n = q2 . n
by A22, A30, A31, FINSEQ_1:def 7;
hence
[(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n)
by A23, A31, A32;
:: thesis: verum
end;
hence
[((Den o,A) . x),((Den o,A) . ((q2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o)
by A11, A14, A16, A19, A21, A29, A30;
:: thesis: verum
end;
A33:
l + 1
in Seg (len a1)
by A12, FINSEQ_1:6;
then A34:
l + 1
in dom a1
by FINSEQ_1:def 3;
A35:
l + 1
in dom a2
by A13, A33, FINSEQ_1:def 3;
A36:
x1 =
a1 . (l + 1)
by A16, A18, FINSEQ_1:59
.=
x . (l + 1)
by A14, A34, FINSEQ_1:def 7
;
y1 =
a2 . (l + 1)
by A17, A20, FINSEQ_1:59
.=
(a2 ^ b1) . (l + 1)
by A35, FINSEQ_1:def 7
;
then
[x1,y1] in C . ((the_arity_of o) /. (l + 1))
by A15, A34, A36;
hence
[((Den o,A) . x),((Den o,A) . (a2 ^ b1))] in C . (the_result_sort_of o)
by A1, A14, A16, A17, A18, A21, A23, A28, Th15;
:: thesis: verum
end;
A37:
for l being Element of NAT holds S1[l]
from NAT_1:sch 1(A3, A10);
A38: dom x =
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
dom y =
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
then reconsider a1 = x, a2 = y as FinSequence by A38, FINSEQ_1:def 2;
set b1 = {} ;
A39: Seg (len a1) =
dom a1
by FINSEQ_1:def 3
.=
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
Seg (len a2) =
dom a2
by FINSEQ_1:def 3
.=
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
then A40:
len a1 = len a2
by A39, FINSEQ_1:8;
A41:
x = a1 ^ {}
by FINSEQ_1:47;
y = a2 ^ {}
by FINSEQ_1:47;
hence
[((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o)
by A2, A37, A40, A41; :: thesis: verum