let D be non empty set ; for X being non empty Subset of D
for f being BinOp of D
for m being Nat st f is associative & X is f -unambiguous holds
(MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous
let X be non empty Subset of D; for f being BinOp of D
for m being Nat st f is associative & X is f -unambiguous holds
(MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous
let f be BinOp of D; for m being Nat st f is associative & X is f -unambiguous holds
(MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous
let m be Nat; ( f is associative & X is f -unambiguous implies (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous )
set F = MultPlace f;
assume A1:
f is associative
; ( not X is f -unambiguous or (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous )
assume A2:
X is f -unambiguous
; (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous
defpred S1[ Nat] means (MultPlace f) .: (($1 + 1) -tuples_on X) is f -unambiguous ;
A3:
S1[ 0 ]
proof
set Z =
(0 + 1) -tuples_on X;
set Y =
(MultPlace f) .: ((0 + 1) -tuples_on X);
for
x,
y,
d1,
d2 being
set st
x in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D &
y in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D &
d1 in D &
d2 in D &
f . (
x,
d1)
= f . (
y,
d2) holds
(
x = y &
d1 = d2 )
proof
let x,
y,
d1,
d2 be
set ;
( x in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D & y in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) implies ( x = y & d1 = d2 ) )
assume
x in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D
;
( not y in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D or not d1 in D or not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) )
then
x in (MultPlace f) .: ((0 + 1) -tuples_on X)
by XBOOLE_0:def 4;
then consider uu being
object such that A4:
(
uu in dom (MultPlace f) &
[uu,x] in MultPlace f &
uu in (0 + 1) -tuples_on X )
by RELAT_1:110;
assume
y in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D
;
( not d1 in D or not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) )
then
y in (MultPlace f) .: ((0 + 1) -tuples_on X)
by XBOOLE_0:def 4;
then consider vv being
object such that A5:
(
vv in dom (MultPlace f) &
[vv,y] in MultPlace f &
vv in (0 + 1) -tuples_on X )
by RELAT_1:110;
assume
d1 in D
;
( not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) )
then reconsider d11 =
d1 as
Element of
D ;
assume
d2 in D
;
( not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) )
then reconsider d22 =
d2 as
Element of
D ;
reconsider u =
uu as
Element of 1
-tuples_on X by A4;
reconsider v =
vv as
Element of 1
-tuples_on X by A5;
assume
f . (
x,
d1)
= f . (
y,
d2)
;
( x = y & d1 = d2 )
then A6:
(
f . (
x,
d1)
= f . (
y,
d2) &
(MultPlace f) . u = x &
(MultPlace f) . v = y )
by A4, A5, FUNCT_1:def 2;
consider ee being
Element of
X such that A7:
u = <*ee*>
by FINSEQ_2:97;
consider ff being
Element of
X such that A8:
v = <*ff*>
by FINSEQ_2:97;
reconsider eee =
ee,
fff =
ff as
Element of
D ;
(
f . (
((MultPlace f) . <*eee*>),
d1)
= f . (
((MultPlace f) . <*fff*>),
d2) &
(MultPlace f) . <*eee*> = eee &
(MultPlace f) . <*fff*> = fff )
by A6, A7, A8, Lm15;
then
(
ee in X /\ D &
ff in X /\ D &
d11 in D &
d22 in D &
f . (
ee,
d11)
= f . (
ff,
d22) )
by XBOOLE_0:def 4;
hence
(
x = y &
d1 = d2 )
by A6, A7, A8, A2;
verum
end;
hence
S1[
0 ]
by Def10;
verum
end;
A9:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A10:
S1[
m]
;
S1[m + 1]
set Z =
((m + 1) + 1) -tuples_on X;
set Y =
(MultPlace f) .: (((m + 1) + 1) -tuples_on X);
for
x,
y,
d1,
d2 being
set st
x in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D &
y in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D &
d1 in D &
d2 in D &
f . (
x,
d1)
= f . (
y,
d2) holds
(
x = y &
d1 = d2 )
proof
let x,
y,
d1,
d2 be
set ;
( x in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D & y in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) implies ( x = y & d1 = d2 ) )
assume
x in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D
;
( not y in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D or not d1 in D or not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) )
then
x in (MultPlace f) .: (((m + 1) + 1) -tuples_on X)
by XBOOLE_0:def 4;
then consider uu being
object such that A11:
(
uu in dom (MultPlace f) &
[uu,x] in MultPlace f &
uu in ((m + 1) + 1) -tuples_on X )
by RELAT_1:110;
assume
y in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D
;
( not d1 in D or not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) )
then
y in (MultPlace f) .: (((m + 1) + 1) -tuples_on X)
by XBOOLE_0:def 4;
then consider vv being
object such that A12:
(
vv in dom (MultPlace f) &
[vv,y] in MultPlace f &
vv in ((m + 1) + 1) -tuples_on X )
by RELAT_1:110;
assume
d1 in D
;
( not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) )
then reconsider d11 =
d1 as
Element of
D ;
assume
d2 in D
;
( not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) )
then reconsider d22 =
d2 as
Element of
D ;
reconsider u =
uu as
Element of
((m + 1) + 1) -tuples_on X by A11;
reconsider v =
vv as
Element of
((m + 1) + 1) -tuples_on X by A12;
(
len u = (m + 1) + 1 &
len v = (m + 1) + 1 &
m + 1
<= (m + 1) + 1 )
by CARD_1:def 7, NAT_1:11;
then A13:
(
u = (u | (m + 1)) ^ <*(u /. (len u))*> &
v = (v | (m + 1)) ^ <*(v /. (len v))*> &
len (u | (m + 1)) = m + 1 &
len (v | (m + 1)) = m + 1 )
by FINSEQ_5:21, FINSEQ_1:59;
then reconsider u1 =
u | (m + 1),
v1 =
v | (m + 1) as
Tuple of
m + 1,
X by CARD_1:def 7;
(
rng u1 c= D &
rng v1 c= D )
by XBOOLE_1:1;
then reconsider u2 =
u1,
v2 =
v1 as non
empty FinSequence of
D by FINSEQ_1:def 4;
reconsider u3 =
u2,
v3 =
v2 as
Element of
(D *) \ {{}} by Th5;
reconsider u4 =
u2,
v4 =
v3 as
Element of
(m + 1) -tuples_on X by FINSEQ_2:131;
reconsider ul =
u /. (len u),
vl =
v /. (len v) as
Element of
D by TARSKI:def 3;
A14:
(
ul in X /\ D &
vl in X /\ D )
by XBOOLE_0:def 4;
A15:
(
(MultPlace f) . (u2 ^ <*ul*>) = f . (
((MultPlace f) . u2),
ul) &
(MultPlace f) . (v2 ^ <*vl*>) = f . (
((MultPlace f) . v2),
vl) )
by Lm15;
A16:
(
f . (
(f . (((MultPlace f) . u3),ul)),
d11)
= f . (
((MultPlace f) . u3),
(f . (ul,d11))) &
f . (
(f . (((MultPlace f) . v3),vl)),
d22)
= f . (
((MultPlace f) . v3),
(f . (vl,d22))) )
by A1;
assume
f . (
x,
d1)
= f . (
y,
d2)
;
( x = y & d1 = d2 )
then A17:
(
f . (
x,
d1)
= f . (
y,
d2) &
(MultPlace f) . u = x &
(MultPlace f) . v = y )
by A11, A12, FUNCT_1:def 2;
dom (MultPlace f) = (D *) \ {{}}
by FUNCT_2:def 1;
then
(
u3 in dom (MultPlace f) &
v3 in dom (MultPlace f) &
u4 in (m + 1) -tuples_on X &
v4 in (m + 1) -tuples_on X )
;
then
(
(MultPlace f) . u4 in (MultPlace f) .: ((m + 1) -tuples_on X) &
(MultPlace f) . v4 in (MultPlace f) .: ((m + 1) -tuples_on X) &
f . (
ul,
d11)
in D &
f . (
vl,
d22)
in D )
by FUNCT_1:def 6;
then
(
(MultPlace f) . u4 in ((MultPlace f) .: ((m + 1) -tuples_on X)) /\ D &
(MultPlace f) . v4 in ((MultPlace f) .: ((m + 1) -tuples_on X)) /\ D &
f . (
ul,
d11)
in D &
f . (
vl,
d22)
in D )
by XBOOLE_0:def 4;
then A18:
(
(MultPlace f) . u3 = (MultPlace f) . v3 &
f . (
ul,
d11)
= f . (
vl,
d22) )
by A17, A13, A15, A16, A10, Def10;
thus
(
x = y &
d1 = d2 )
by A18, A2, A14, A17, A13, A15;
verum
end;
hence
S1[
m + 1]
by Def10;
verum
end;
for m being Nat holds S1[m]
from NAT_1:sch 2(A3, A9);
hence
(MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous
; verum