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;
A1: dom (MultPlace f) = (D *) \ {{}} by FUNCT_2:def 1;
defpred S1[ Nat] means MultPlace f is ($1 + 1) -tuples_on X -one-to-one ;
assume A2: ( f is associative & X is f -unambiguous ) ; :: thesis: MultPlace f is (m + 1) -tuples_on X -one-to-one
A3: S1[ 0 ]
proof
now :: thesis: for x, y being set st 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 holds
x = y
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 A4: ( 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 A5: ( 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
A6: x = <*u*> by FINSEQ_2:97, A5;
consider v being Element of X such that
A7: y = <*v*> by FINSEQ_2:97, A5;
reconsider uu = u, vv = v as Element of D ;
uu = (MultPlace f) . y by A4, A6, Lm15
.= vv by A7, Lm15 ;
hence x = y by A6, A7; :: thesis: verum
end;
hence MultPlace f is (0 + 1) -tuples_on X -one-to-one ; :: thesis: verum
end;
A8: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A9: S1[m] ; :: thesis: S1[m + 1]
set goal = ((m + 1) + 1) -tuples_on X;
now :: thesis: for x, y being set st 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 holds
x = y
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 A10: ( 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 XBOOLE_0:def 4, A10;
( 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;
A11: ( (MultPlace f) . (x111 ^ <*xl*>) = f . (((MultPlace f) . x111),xl) & (MultPlace f) . (y111 ^ <*yl*>) = f . (((MultPlace f) . y111),yl) ) by Lm15;
( len xx = (m + 1) + 1 & len yy = (m + 1) + 1 ) by CARD_1:def 7;
then A12: ( xx = x1 ^ <*xl*> & yy = y1 ^ <*yl*> ) by FINSEQ_5:21;
A13: ( 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 Th5, A1;
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 PARTFUN1:4, FUNCT_1:def 6;
then A14: ( (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 XBOOLE_0:def 4, A12, A11, A10;
(MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous by A2, Lm18;
then A15: ( (MultPlace f) . x1 = (MultPlace f) . y1 & xl = yl ) by A14;
( x1 in ((m + 1) -tuples_on X) /\ (dom (MultPlace f)) & y1 in ((m + 1) -tuples_on X) /\ (dom (MultPlace f)) ) by A13, XBOOLE_0:def 4;
hence x = y by A15, A9, Def6, A12; :: thesis: verum
end;
hence MultPlace f is ((m + 1) + 1) -tuples_on X -one-to-one ; :: thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch 2(A3, A8);
 hence MultPlace f is (m + 1) -tuples_on X -one-to-one ; :: thesis: verum