let Y be set ; :: thesis: for D being non empty 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 D be non empty 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 )
assume A1: ( f is associative & Y is f -unambiguous ) ; :: thesis: MultPlace f is (m + 1) -tuples_on Y -one-to-one
set F = MultPlace f;
A2: (MultPlace f) | ((m + 1) -tuples_on Y) = ((MultPlace f) | ((D *) \ {{}})) | ((m + 1) -tuples_on Y)
.= (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 Lm6
.= (MultPlace f) | ((D *) /\ ((m + 1) -tuples_on Y)) by XBOOLE_1:83, Lm5
.= (MultPlace f) | ((m + 1) -tuples_on (Y /\ D)) by Th2 ;
A3: Y /\ D is f -unambiguous by Lm11, A1, 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 Lm20, A3, A1;
then (MultPlace f) | ((m + 1) -tuples_on Y) is one-to-one by A2;
hence MultPlace f is (m + 1) -tuples_on Y -one-to-one ; :: 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 A2; :: thesis: verum

end;

end;