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 x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (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 x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let o be OperSymbol of S; for C1, C2 being MSCongruence of A
for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let C1, C2 be MSCongruence of A; for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let x1, y1 be set ; for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let a1, b1 be FinSequence; ( [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) implies for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) )
assume A1:
[x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1)))
; for x, y being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
let x, y be Element of Args (o,A); ( x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 implies [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o)) )
assume that
A2:
x = (a1 ^ <*x1*>) ^ b1
and
A3:
y = (a1 ^ <*y1*>) ^ b1
; [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
A4:
y = a1 ^ (<*y1*> ^ b1)
by A3, FINSEQ_1:32;
A5:
x = a1 ^ (<*x1*> ^ b1)
by A2, FINSEQ_1:32;
now [((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))per cases
( [x1,y1] in C1 . ((the_arity_of o) /. ((len a1) + 1)) or [x1,y1] in C2 . ((the_arity_of o) /. ((len a1) + 1)) )
by A1, XBOOLE_0:def 3;
suppose A6:
[x1,y1] in C1 . ((the_arity_of o) /. ((len a1) + 1))
;
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
for
n being
Nat st
n in dom x holds
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
proof
let n be
Nat;
( n in dom x implies [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) )
assume A7:
n in dom x
;
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
then reconsider dz =
dom (the_arity_of o) as non
empty set by MSUALG_3:6;
A8:
n in dom (the_arity_of o)
by A7, MSUALG_3:6;
then A9:
n in dom ( the Sorts of A * (the_arity_of o))
by PARTFUN1:def 2;
reconsider so = the
Sorts of
A * (the_arity_of o) as
V2()
ManySortedSet of
dz ;
A10:
not
product so is
empty
;
pi (
(Args (o,A)),
n) =
pi (
((( the Sorts of A #) * the Arity of S) . o),
n)
by MSUALG_1:def 4
.=
pi (
(( the Sorts of A #) . ( the Arity of S . o)),
n)
by FUNCT_2:15
.=
pi (
(( the Sorts of A #) . (the_arity_of o)),
n)
by MSUALG_1:def 1
.=
pi (
(product ( the Sorts of A * (the_arity_of o))),
n)
by FINSEQ_2:def 5
.=
( the Sorts of A * (the_arity_of o)) . n
by A9, A10, CARD_3:12
.=
the
Sorts of
A . ((the_arity_of o) . n)
by A8, FUNCT_1:13
.=
the
Sorts of
A . ((the_arity_of o) /. n)
by A8, PARTFUN1:def 6
;
then A11:
x . n in the
Sorts of
A . ((the_arity_of o) /. n)
by CARD_3:def 6;
A12:
(
n in dom (a1 ^ <*x1*>) or ex
k being
Nat st
(
k in dom b1 &
n = (len (a1 ^ <*x1*>)) + k ) )
by A2, A7, FINSEQ_1:25;
now [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)per cases
( n in dom a1 or ex m being Nat st
( m in dom <*x1*> & n = (len a1) + m ) or ex k being Element of NAT st
( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) )
by A12, FINSEQ_1:25;
suppose
ex
m being
Nat st
(
m in dom <*x1*> &
n = (len a1) + m )
;
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)then consider m being
Nat such that A15:
m in dom <*x1*>
and A16:
n = (len a1) + m
;
A17:
m in Seg 1
by A15, FINSEQ_1:38;
then A18:
m = 1
by FINSEQ_1:2, TARSKI:def 1;
then A19:
n in Seg ((len a1) + 1)
by A16, FINSEQ_1:4;
then
n in Seg ((len a1) + (len <*y1*>))
by FINSEQ_1:40;
then
n in Seg (len (a1 ^ <*y1*>))
by FINSEQ_1:22;
then
n in dom (a1 ^ <*y1*>)
by FINSEQ_1:def 3;
then A20:
y . n =
(a1 ^ <*y1*>) . ((len a1) + 1)
by A3, A16, A18, FINSEQ_1:def 7
.=
y1
by FINSEQ_1:42
;
n in Seg ((len a1) + (len <*x1*>))
by A19, FINSEQ_1:40;
then
n in Seg (len (a1 ^ <*x1*>))
by FINSEQ_1:22;
then
n in dom (a1 ^ <*x1*>)
by FINSEQ_1:def 3;
then x . n =
(a1 ^ <*x1*>) . ((len a1) + 1)
by A2, A16, A18, FINSEQ_1:def 7
.=
x1
by FINSEQ_1:42
;
hence
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
by A6, A16, A17, A20, FINSEQ_1:2, TARSKI:def 1;
verum end; end; end;
hence
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
;
verum
end; then
[((Den (o,A)) . x),((Den (o,A)) . y)] in C1 . (the_result_sort_of o)
by MSUALG_4:def 4;
hence
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
by XBOOLE_0:def 3;
verum end; suppose A24:
[x1,y1] in C2 . ((the_arity_of o) /. ((len a1) + 1))
;
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
for
n being
Nat st
n in dom x holds
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
proof
let n be
Nat;
( n in dom x implies [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) )
assume A25:
n in dom x
;
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
then reconsider dz =
dom (the_arity_of o) as non
empty set by MSUALG_3:6;
A26:
n in dom (the_arity_of o)
by A25, MSUALG_3:6;
then A27:
n in dom ( the Sorts of A * (the_arity_of o))
by PARTFUN1:def 2;
reconsider so = the
Sorts of
A * (the_arity_of o) as
V2()
ManySortedSet of
dz ;
A28:
not
product so is
empty
;
pi (
(Args (o,A)),
n) =
pi (
((( the Sorts of A #) * the Arity of S) . o),
n)
by MSUALG_1:def 4
.=
pi (
(( the Sorts of A #) . ( the Arity of S . o)),
n)
by FUNCT_2:15
.=
pi (
(( the Sorts of A #) . (the_arity_of o)),
n)
by MSUALG_1:def 1
.=
pi (
(product ( the Sorts of A * (the_arity_of o))),
n)
by FINSEQ_2:def 5
.=
( the Sorts of A * (the_arity_of o)) . n
by A27, A28, CARD_3:12
.=
the
Sorts of
A . ((the_arity_of o) . n)
by A26, FUNCT_1:13
.=
the
Sorts of
A . ((the_arity_of o) /. n)
by A26, PARTFUN1:def 6
;
then A29:
x . n in the
Sorts of
A . ((the_arity_of o) /. n)
by CARD_3:def 6;
A30:
(
n in dom (a1 ^ <*x1*>) or ex
k being
Nat st
(
k in dom b1 &
n = (len (a1 ^ <*x1*>)) + k ) )
by A2, A25, FINSEQ_1:25;
now [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)per cases
( n in dom a1 or ex m being Nat st
( m in dom <*x1*> & n = (len a1) + m ) or ex k being Element of NAT st
( k in dom b1 & n = (len (a1 ^ <*x1*>)) + k ) )
by A30, FINSEQ_1:25;
suppose
ex
m being
Nat st
(
m in dom <*x1*> &
n = (len a1) + m )
;
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)then consider m being
Nat such that A33:
m in dom <*x1*>
and A34:
n = (len a1) + m
;
A35:
m in Seg 1
by A33, FINSEQ_1:38;
then A36:
m = 1
by FINSEQ_1:2, TARSKI:def 1;
then A37:
n in Seg ((len a1) + 1)
by A34, FINSEQ_1:4;
then
n in Seg ((len a1) + (len <*y1*>))
by FINSEQ_1:40;
then
n in Seg (len (a1 ^ <*y1*>))
by FINSEQ_1:22;
then
n in dom (a1 ^ <*y1*>)
by FINSEQ_1:def 3;
then A38:
y . n =
(a1 ^ <*y1*>) . ((len a1) + 1)
by A3, A34, A36, FINSEQ_1:def 7
.=
y1
by FINSEQ_1:42
;
n in Seg ((len a1) + (len <*x1*>))
by A37, FINSEQ_1:40;
then
n in Seg (len (a1 ^ <*x1*>))
by FINSEQ_1:22;
then
n in dom (a1 ^ <*x1*>)
by FINSEQ_1:def 3;
then x . n =
(a1 ^ <*x1*>) . ((len a1) + 1)
by A2, A34, A36, FINSEQ_1:def 7
.=
x1
by FINSEQ_1:42
;
hence
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
by A24, A34, A35, A38, FINSEQ_1:2, TARSKI:def 1;
verum end; end; end;
hence
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
;
verum
end; then
[((Den (o,A)) . x),((Den (o,A)) . y)] in C2 . (the_result_sort_of o)
by MSUALG_4:def 4;
hence
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
by XBOOLE_0:def 3;
verum end; end; end;
hence
[((Den (o,A)) . x),((Den (o,A)) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
; verum