let D be non empty set ; :: thesis:
let X be non empty Subset of D; :: thesis:
let f be BinOp of D; :: thesis:
let m be Nat; :: thesis:
set F = MultPlace f;
assume A1: f is associative ; :: thesis:
assume A2: X is f -unambiguous ; :: thesis:
defpred S₁[ Nat] means (MultPlace f) .: (($1 + 1) -tuples_on X) is f -unambiguous ;
A3: S₁[ 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 ; :: thesis:
assume x in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
then reconsider d11 = d1 as Element of D ;
assume d2 in D ; :: thesis:
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) ; :: thesis:
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; :: thesis:

end;

hence S₁[ 0 ] by Def10; :: thesis:

end;

A9: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis:
assume A10: S₁[m] ; :: thesis:
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 ; :: thesis:
assume x in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
then reconsider d11 = d1 as Element of D ;
assume d2 in D ; :: thesis:
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) ; :: thesis:
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; :: thesis:

end;

hence S₁[m + 1] by Def10; :: thesis:

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A3, A9);
hence (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous ; :: thesis: