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) .: ((m + 1) -tuples_on Y) is f -unambiguous
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) .: ((m + 1) -tuples_on Y) is f -unambiguous
let f be BinOp of D; :: thesis: for m being Nat st f is associative & Y is f -unambiguous holds
(MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous
let m be Nat; :: thesis: ( f is associative & Y is f -unambiguous implies (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous )
set F = MultPlace f;
A1: dom (MultPlace f) = (D *) \ {{}} by FUNCT_2:def 1;
assume ( f is associative & Y is f -unambiguous ) ; :: thesis: (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous
then A2: ( f is associative & Y /\ D is f -unambiguous ) by XBOOLE_1:17, Lm11;
A3: (MultPlace f) .: ((m + 1) -tuples_on Y) = (MultPlace f) .: (((D *) \ {{}}) /\ ((m + 1) -tuples_on Y)) by A1, RELAT_1:112
.= (MultPlace f) .: (((D *) /\ ((m + 1) -tuples_on Y)) \ {{}}) by XBOOLE_1:49
.= (MultPlace f) .: (((m + 1) -tuples_on (Y /\ D)) \ {{}}) by Th2
.= (MultPlace f) .: (((m + 1) -tuples_on (Y /\ D)) \ (0 -tuples_on Y)) by Lm6
.= (MultPlace f) .: ((m + 1) -tuples_on (Y /\ D)) by Lm5, XBOOLE_1:83 ;

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

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

then reconsider YY = Y /\ D as non empty Subset of D by XBOOLE_1:17;
(MultPlace f) .: ((m + 1) -tuples_on Y) = (MultPlace f) .: ((m + 1) -tuples_on YY) by A3;
hence (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous by Lm18, A2; :: thesis: verum

end;

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

then (MultPlace f) .: ((m + 1) -tuples_on Y) = {} by A3;
hence (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous ; :: thesis: verum

end;

end;