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 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 of S; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( [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)))
; :: thesis: 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; :: thesis: ( 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 A2:
( x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 )
; :: thesis: [((Den o,A) . x),((Den o,A) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
then A3:
( x = a1 ^ (<*x1*> ^ b1) & y = a1 ^ (<*y1*> ^ b1) )
by FINSEQ_1:45;
now 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 A4:
[x1,y1] in C1 . ((the_arity_of o) /. ((len a1) + 1))
;
:: thesis: [((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;
:: thesis: ( n in dom x implies [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) )
assume A5:
n in dom x
;
:: thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
then A6:
(
n in dom (a1 ^ <*x1*>) or ex
k being
Nat st
(
k in dom b1 &
n = (len (a1 ^ <*x1*>)) + k ) )
by A2, FINSEQ_1:38;
A8:
n in dom (the_arity_of o)
by A5, MSUALG_3:6;
then A9:
n in dom (the Sorts of A * (the_arity_of o))
by PARTFUN1:def 4;
reconsider dz =
dom (the_arity_of o) as non
empty set by A5, MSUALG_3:6;
reconsider so = the
Sorts of
A * (the_arity_of o) as
V2()
ManySortedSet of ;
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 9
.=
pi ((the Sorts of A # ) . (the Arity of S . o)),
n
by FUNCT_2:21
.=
pi ((the Sorts of A # ) . (the_arity_of o)),
n
by MSUALG_1:def 6
.=
pi (product (the Sorts of A * (the_arity_of o))),
n
by PBOOLE:def 19
.=
(the Sorts of A * (the_arity_of o)) . n
by A9, A10, CARD_3:22
.=
the
Sorts of
A . ((the_arity_of o) . n)
by A8, FUNCT_1:23
.=
the
Sorts of
A . ((the_arity_of o) /. n)
by A8, PARTFUN1:def 8
;
then A11:
x . n in the
Sorts of
A . ((the_arity_of o) /. n)
by CARD_3:def 6;
now 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 A6, FINSEQ_1:38;
suppose
ex
m being
Nat st
(
m in dom <*x1*> &
n = (len a1) + m )
;
:: thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)then consider m being
Nat such that A14:
(
m in dom <*x1*> &
n = (len a1) + m )
;
A15:
m in Seg 1
by A14, FINSEQ_1:55;
then A16:
m = 1
by FINSEQ_1:4, TARSKI:def 1;
then A17:
n in Seg ((len a1) + 1)
by A14, FINSEQ_1:6;
then
n in Seg ((len a1) + (len <*x1*>))
by FINSEQ_1:57;
then
n in Seg (len (a1 ^ <*x1*>))
by FINSEQ_1:35;
then A18:
n in dom (a1 ^ <*x1*>)
by FINSEQ_1:def 3;
n in Seg ((len a1) + (len <*y1*>))
by A17, FINSEQ_1:57;
then
n in Seg (len (a1 ^ <*y1*>))
by FINSEQ_1:35;
then A19:
n in dom (a1 ^ <*y1*>)
by FINSEQ_1:def 3;
A20:
x . n =
(a1 ^ <*x1*>) . ((len a1) + 1)
by A2, A14, A16, A18, FINSEQ_1:def 7
.=
x1
by FINSEQ_1:59
;
y . n =
(a1 ^ <*y1*>) . ((len a1) + 1)
by A2, A14, A16, A19, FINSEQ_1:def 7
.=
y1
by FINSEQ_1:59
;
hence
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
by A4, A14, A15, A20, FINSEQ_1:4, TARSKI:def 1;
:: thesis: verum end;
hence
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
;
:: thesis: verum
end; then
[((Den o,A) . x),((Den o,A) . y)] in C1 . (the_result_sort_of o)
by MSUALG_4:def 6;
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;
:: thesis: verum suppose A23:
[x1,y1] in C2 . ((the_arity_of o) /. ((len a1) + 1))
;
:: thesis: [((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;
:: thesis: ( n in dom x implies [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) )
assume A24:
n in dom x
;
:: thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
then A25:
(
n in dom (a1 ^ <*x1*>) or ex
k being
Nat st
(
k in dom b1 &
n = (len (a1 ^ <*x1*>)) + k ) )
by A2, FINSEQ_1:38;
A27:
n in dom (the_arity_of o)
by A24, MSUALG_3:6;
then A28:
n in dom (the Sorts of A * (the_arity_of o))
by PARTFUN1:def 4;
reconsider dz =
dom (the_arity_of o) as non
empty set by A24, MSUALG_3:6;
reconsider so = the
Sorts of
A * (the_arity_of o) as
V2()
ManySortedSet of ;
A29:
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 9
.=
pi ((the Sorts of A # ) . (the Arity of S . o)),
n
by FUNCT_2:21
.=
pi ((the Sorts of A # ) . (the_arity_of o)),
n
by MSUALG_1:def 6
.=
pi (product (the Sorts of A * (the_arity_of o))),
n
by PBOOLE:def 19
.=
(the Sorts of A * (the_arity_of o)) . n
by A28, A29, CARD_3:22
.=
the
Sorts of
A . ((the_arity_of o) . n)
by A27, FUNCT_1:23
.=
the
Sorts of
A . ((the_arity_of o) /. n)
by A27, PARTFUN1:def 8
;
then A30:
x . n in the
Sorts of
A . ((the_arity_of o) /. n)
by CARD_3:def 6;
now 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 A25, FINSEQ_1:38;
suppose
ex
m being
Nat st
(
m in dom <*x1*> &
n = (len a1) + m )
;
:: thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)then consider m being
Nat such that A33:
(
m in dom <*x1*> &
n = (len a1) + m )
;
A34:
m in Seg 1
by A33, FINSEQ_1:55;
then A35:
m = 1
by FINSEQ_1:4, TARSKI:def 1;
then A36:
n in Seg ((len a1) + 1)
by A33, FINSEQ_1:6;
then
n in Seg ((len a1) + (len <*x1*>))
by FINSEQ_1:57;
then
n in Seg (len (a1 ^ <*x1*>))
by FINSEQ_1:35;
then A37:
n in dom (a1 ^ <*x1*>)
by FINSEQ_1:def 3;
n in Seg ((len a1) + (len <*y1*>))
by A36, FINSEQ_1:57;
then
n in Seg (len (a1 ^ <*y1*>))
by FINSEQ_1:35;
then A38:
n in dom (a1 ^ <*y1*>)
by FINSEQ_1:def 3;
A39:
x . n =
(a1 ^ <*x1*>) . ((len a1) + 1)
by A2, A33, A35, A37, FINSEQ_1:def 7
.=
x1
by FINSEQ_1:59
;
y . n =
(a1 ^ <*y1*>) . ((len a1) + 1)
by A2, A33, A35, A38, FINSEQ_1:def 7
.=
y1
by FINSEQ_1:59
;
hence
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
by A23, A33, A34, A39, FINSEQ_1:4, TARSKI:def 1;
:: thesis: verum end;
hence
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
;
:: thesis: verum
end; then
[((Den o,A) . x),((Den o,A) . y)] in C2 . (the_result_sort_of o)
by MSUALG_4:def 6;
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;
:: thesis: verum
hence
[((Den o,A) . x),((Den o,A) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))
; :: thesis: verum