let D be non empty set ; :: thesis: 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 is (m + 1) -tuples_on X -one-to-one
let X be non empty Subset of D; :: thesis: for f being BinOp of D
for m being Nat st f is associative & X is f -unambiguous holds
MultPlace f is (m + 1) -tuples_on X -one-to-one
let f be BinOp of D; :: thesis: for m being Nat st f is associative & X is f -unambiguous holds
MultPlace f is (m + 1) -tuples_on X -one-to-one
let m be Nat; :: thesis: ( f is associative & X is f -unambiguous implies MultPlace f is (m + 1) -tuples_on X -one-to-one )
set F = MultPlace f;
A0: dom (MultPlace f) = (D *) \ {{}} by FUNCT_2:def 1;
defpred S₁[ Nat] means MultPlace f is ($1 + 1) -tuples_on X -one-to-one ;
assume Z2: ( f is associative & X is f -unambiguous ) ; :: thesis: MultPlace f is (m + 1) -tuples_on X -one-to-one
A10: S₁[ 0 ]

proof

now

let x, y be set ; :: thesis: ( x in ((0 + 1) -tuples_on X) /\ (dom (MultPlace f)) & y in ((0 + 1) -tuples_on X) /\ (dom (MultPlace f)) & (MultPlace f) . x = (MultPlace f) . y implies x = y )
assume Z3: ( x in ((0 + 1) -tuples_on X) /\ (dom (MultPlace f)) & y in ((0 + 1) -tuples_on X) /\ (dom (MultPlace f)) & (MultPlace f) . x = (MultPlace f) . y ) ; :: thesis: x = y
then Z1: ( x is Element of 1 -tuples_on X & y is Element of 1 -tuples_on X & (MultPlace f) . x = (MultPlace f) . y ) by XBOOLE_0:def 4;
consider u being Element of X such that
C3: x = <*u*> by Z1, FINSEQ_2:97;
consider v being Element of X such that
C4: y = <*v*> by Z1, FINSEQ_2:97;
reconsider uu = u, vv = v as Element of D ;
uu = (MultPlace f) . y by Z3, C3, LmMultPlace
.= vv by C4, LmMultPlace ;
hence x = y by C3, C4; :: thesis: verum

end;

hence MultPlace f is (0 + 1) -tuples_on X -one-to-one by DefInj2; :: thesis: verum

end;

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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume B1: S₁[m] ; :: thesis: S₁[m + 1]
set goal = ((m + 1) + 1) -tuples_on X;

now

let x, y be set ; :: thesis: ( x in (((m + 1) + 1) -tuples_on X) /\ (dom (MultPlace f)) & y in (((m + 1) + 1) -tuples_on X) /\ (dom (MultPlace f)) & (MultPlace f) . x = (MultPlace f) . y implies x = y )
assume Z1: ( x in (((m + 1) + 1) -tuples_on X) /\ (dom (MultPlace f)) & y in (((m + 1) + 1) -tuples_on X) /\ (dom (MultPlace f)) & (MultPlace f) . x = (MultPlace f) . y ) ; :: thesis: x = y
reconsider xx = x, yy = y as Element of ((m + 1) + 1) -tuples_on X by Z1, XBOOLE_0:def 4;
( len xx = (m + 1) + 1 & len yy = (m + 1) + 1 & (m + 1) + 0 <= (m + 1) + 1 ) by CARD_1:def 7, NAT_1:11;
then ( len (xx | (m + 1)) = m + 1 & len (yy | (m + 1)) = m + 1 ) by FINSEQ_1:59;
then reconsider x1 = xx | (m + 1), y1 = yy | (m + 1) as Element of (m + 1) -tuples_on X by FINSEQ_2:92;
reconsider x11 = x1, y11 = y1 as non empty FinSequence of X ;
( rng x11 c= D & rng y11 c= D ) by XBOOLE_1:1;
then reconsider x111 = x11, y111 = y11 as non empty FinSequence of D by FINSEQ_1:def 4;
reconsider xl = xx /. (len xx), yl = yy /. (len yy) as Element of D by TARSKI:def 3;
C2: ( (MultPlace f) . (x111 ^ <*xl*>) = f . (((MultPlace f) . x111),xl) & (MultPlace f) . (y111 ^ <*yl*>) = f . (((MultPlace f) . y111),yl) ) by LmMultPlace;
( len xx = (m + 1) + 1 & len yy = (m + 1) + 1 ) by CARD_1:def 7;
then C10: ( xx = x1 ^ <*xl*> & yy = y1 ^ <*yl*> ) by FINSEQ_5:21;
C7: ( x111 in dom (MultPlace f) & x1 in (m + 1) -tuples_on X & y111 in dom (MultPlace f) & y1 in (m + 1) -tuples_on X ) by Lm2, A0;
then ( (MultPlace f) . x1 in (MultPlace f) .: ((m + 1) -tuples_on X) & (MultPlace f) . x111 in D & (MultPlace f) . y1 in (MultPlace f) .: ((m + 1) -tuples_on X) & (MultPlace f) . y111 in D ) by FUNCT_1:def 6, PARTFUN1:4;
then C4: ( (MultPlace f) . x1 in ((MultPlace f) .: ((m + 1) -tuples_on X)) /\ D & (MultPlace f) . y1 in ((MultPlace f) .: ((m + 1) -tuples_on X)) /\ D & xl in D & yl in D & f . (((MultPlace f) . x1),xl) = f . (((MultPlace f) . y1),yl) ) by C10, C2, Z1, XBOOLE_0:def 4;
(MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous by Z2, Lm5;
then C8: ( (MultPlace f) . x1 = (MultPlace f) . y1 & xl = yl ) by C4, DefUnambiguous2;
( x1 in ((m + 1) -tuples_on X) /\ (dom (MultPlace f)) & y1 in ((m + 1) -tuples_on X) /\ (dom (MultPlace f)) ) by C7, XBOOLE_0:def 4;
hence x = y by C8, B1, DefInj2, C10; :: thesis: verum

end;

hence MultPlace f is ((m + 1) + 1) -tuples_on X -one-to-one by DefInj2; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A10, A11);
hence MultPlace f is (m + 1) -tuples_on X -one-to-one ; :: thesis: verum