let D be non empty set ; :: thesis: for Y being set
for f being BinOp of D
for m being Nat st f is associative & Y is f -unambiguous holds
MultPlace f is (m + 1) -tuples_on Y -one-to-one
let Y be set ; :: thesis: for f being BinOp of D
for m being Nat st f is associative & Y is f -unambiguous holds
MultPlace f is (m + 1) -tuples_on Y -one-to-one
let f be BinOp of D; :: thesis: for m being Nat st f is associative & Y is f -unambiguous holds
MultPlace f is (m + 1) -tuples_on Y -one-to-one
let m be Nat; :: thesis: ( f is associative & Y is f -unambiguous implies MultPlace f is (m + 1) -tuples_on Y -one-to-one )
A0: (m + 1) -tuples_on Y misses 0 -tuples_on Y by Lm18;
assume B0: ( f is associative & Y is f -unambiguous ) ; :: thesis: MultPlace f is (m + 1) -tuples_on Y -one-to-one
set F = MultPlace f;
dom (MultPlace f) = (D *) \ {{}} by FUNCT_2:def 1;
then Z1: (MultPlace f) | ((m + 1) -tuples_on Y) = ((MultPlace f) | ((D *) \ {{}})) | ((m + 1) -tuples_on Y) by RELAT_1:69
.= (MultPlace f) | (((D *) \ {{}}) /\ ((m + 1) -tuples_on Y)) by RELAT_1:71
.= (MultPlace f) | (((D *) /\ ((m + 1) -tuples_on Y)) \ {{}}) by XBOOLE_1:49
.= (MultPlace f) | ((D *) /\ (((m + 1) -tuples_on Y) \ {{}})) by XBOOLE_1:49
.= (MultPlace f) | ((D *) /\ (((m + 1) -tuples_on Y) \ (0 -tuples_on Y))) by COMPUT_1:5
.= (MultPlace f) | ((D *) /\ ((m + 1) -tuples_on Y)) by A0, XBOOLE_1:83
.= (MultPlace f) | ((m + 1) -tuples_on (Y /\ D)) by Lm23 ;
B2: Y /\ D is f -unambiguous by Lm13, B0, XBOOLE_1:17;

per cases ( D /\ Y <> {} or D /\ Y = {} ) ;

suppose D /\ Y <> {} ; :: thesis: MultPlace f is (m + 1) -tuples_on Y -one-to-one

then reconsider X = D /\ Y as non empty Subset of D by XBOOLE_1:17;
MultPlace f is (m + 1) -tuples_on X -one-to-one by Lm17, B2, B0;
then (MultPlace f) | ((m + 1) -tuples_on Y) is one-to-one by DefInj1, Z1;
hence MultPlace f is (m + 1) -tuples_on Y -one-to-one by DefInj1; :: thesis: verum

end;

suppose D /\ Y = {} ; :: thesis: MultPlace f is (m + 1) -tuples_on Y -one-to-one

hence MultPlace f is (m + 1) -tuples_on Y -one-to-one by Z1, DefInj1; :: thesis: verum

end;

end;