let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over 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 over 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)
set b1 = {} ;
let o be 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 C1, C2 be 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 C be MSEquivalence-like ManySortedRelation of A; ( 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
; 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); ( ( 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) )
defpred S1[ 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);
A2:
for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be
Nat;
( S1[l] implies S1[l + 1] )
assume A3:
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)
;
S1[l + 1]
let a1,
a2,
b1 be
FinSequence;
( 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 A4:
len a1 = l + 1
and A5:
len a1 = len a2
and A6:
x = a1 ^ b1
and A7:
for
n being
Nat st
n in dom a1 holds
[(x . n),((a2 ^ b1) . n)] in C . ((the_arity_of o) /. n)
;
[((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o)
A8:
l + 1
in Seg (len a1)
by A4, FINSEQ_1:4;
then A9:
l + 1
in dom a2
by A5, FINSEQ_1:def 3;
set y =
a2 ^ b1;
a2 <> {}
by A4, A5;
then consider q2 being
FinSequence,
y1 being
object such that A10:
a2 = q2 ^ <*y1*>
by FINSEQ_1:46;
A11:
l + 1 =
(len q2) + (len <*y1*>)
by A4, A5, A10, FINSEQ_1:22
.=
(len q2) + 1
by FINSEQ_1:40
;
then A12:
y1 =
a2 . (l + 1)
by A10, FINSEQ_1:42
.=
(a2 ^ b1) . (l + 1)
by A9, FINSEQ_1:def 7
;
a1 <> {}
by A4;
then consider q1 being
FinSequence,
x1 being
object such that A13:
a1 = q1 ^ <*x1*>
by FINSEQ_1:46;
A14:
l + 1 =
(len q1) + (len <*x1*>)
by A4, A13, FINSEQ_1:22
.=
(len q1) + 1
by FINSEQ_1:40
;
then A15:
len q1 = len q2
by A11, XCMPLX_1:2;
A16:
dom q1 =
Seg (len q1)
by FINSEQ_1:def 3
.=
dom q2
by A15, FINSEQ_1:def 3
;
A17:
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 ;
( n in dom q1 implies [(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n) )
len q1 <= len a1
by A4, A14, NAT_1:11;
then A18:
Seg (len q1) c= Seg (len a1)
by FINSEQ_1:5;
assume A19:
n in dom q1
;
[(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n)
then
n in Seg (len q1)
by FINSEQ_1:def 3;
then
n in Seg (len a1)
by A18;
then A20:
n in dom a1
by FINSEQ_1:def 3;
then A21:
x . n =
a1 . n
by A6, FINSEQ_1:def 7
.=
q1 . n
by A13, A19, FINSEQ_1:def 7
;
dom a1 =
Seg (len a1)
by FINSEQ_1:def 3
.=
dom a2
by A5, FINSEQ_1:def 3
;
then (a2 ^ b1) . n =
a2 . n
by A20, FINSEQ_1:def 7
.=
q2 . n
by A10, A16, A19, FINSEQ_1:def 7
;
hence
[(q1 . n),(q2 . n)] in C . ((the_arity_of o) /. n)
by A7, A20, A21;
verum
end;
A22:
l + 1
in dom a1
by A8, FINSEQ_1:def 3;
A23:
(q1 ^ <*x1*>) ^ b1 = q1 ^ (<*x1*> ^ b1)
by FINSEQ_1:32;
A24:
(q2 ^ <*x1*>) ^ b1 = q2 ^ (<*x1*> ^ b1)
by FINSEQ_1:32;
A25:
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;
( n in dom q1 implies [(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n) )
assume A26:
n in dom q1
;
[(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n)
then A27:
((q2 ^ <*x1*>) ^ b1) . n = q2 . n
by A16, A24, FINSEQ_1:def 7;
x . n = q1 . n
by A6, A13, A23, A26, FINSEQ_1:def 7;
hence
[(x . n),(((q2 ^ <*x1*>) ^ b1) . n)] in C . ((the_arity_of o) /. n)
by A17, A26, A27;
verum
end;
x1 =
a1 . (l + 1)
by A13, A14, FINSEQ_1:42
.=
x . (l + 1)
by A6, A22, FINSEQ_1:def 7
;
then A28:
[x1,y1] in C . ((the_arity_of o) /. (l + 1))
by A7, A22, A12;
len q1 = l
by A14, XCMPLX_1:2;
then
[((Den (o,A)) . x),((Den (o,A)) . ((q2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o)
by A3, A6, A13, A15, A23, A24, A25;
hence
[((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o)
by A1, A6, A13, A10, A14, A15, A17, A28, Th13;
verum
end;
A29: dom y =
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
dom x =
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 A29, FINSEQ_1:def 2;
assume A30:
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n)
; [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
A31: 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
;
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
;
then A32:
len a1 = len a2
by A31, FINSEQ_1:6;
A33:
x = a1 ^ {}
by FINSEQ_1:34;
A34:
y = a2 ^ {}
by FINSEQ_1:34;
A35:
S1[ 0 ]
proof
field (C . (the_result_sort_of o)) = the
Sorts of
A . (the_result_sort_of o)
by ORDERS_1:12;
then A36:
C . (the_result_sort_of o) is_reflexive_in the
Sorts of
A . (the_result_sort_of o)
by RELAT_2:def 9;
A37: the
Sorts of
A . (the_result_sort_of o) =
the
Sorts of
A . ( the ResultSort of S . o)
by MSUALG_1:def 2
.=
( the Sorts of A * the ResultSort of S) . o
by FUNCT_2:15
.=
Result (
o,
A)
by MSUALG_1:def 5
;
let a1,
a2,
b1 be
FinSequence;
( 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 A38:
len a1 = 0
and A39:
len a1 = len a2
and A40:
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)
;
[((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o)
A41:
a1 = {}
by A38;
a2 = {}
by A38, A39;
hence
[((Den (o,A)) . x),((Den (o,A)) . (a2 ^ b1))] in C . (the_result_sort_of o)
by A40, A41, A37, A36, RELAT_2:def 1;
verum
end;
for l being Nat holds S1[l]
from NAT_1:sch 2(A35, A2);
hence
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
by A30, A32, A33, A34; verum