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) .: ((m + 1) -tuples_on Y) is f -unambiguous
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) .: ((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;
B1: 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 B0: ( f is associative & Y /\ D is f -unambiguous ) by Lm13, XBOOLE_1:17;
B2: (m + 1) -tuples_on (Y /\ D) misses 0 -tuples_on Y by Lm18;
Z1: (MultPlace f) .: ((m + 1) -tuples_on Y) = (MultPlace f) .: (((D *) \ {{}}) /\ ((m + 1) -tuples_on Y)) by B1, RELAT_1:112
.= (MultPlace f) .: (((D *) /\ ((m + 1) -tuples_on Y)) \ {{}}) by XBOOLE_1:49
.= (MultPlace f) .: (((m + 1) -tuples_on (Y /\ D)) \ {{}}) by Lm23
.= (MultPlace f) .: (((m + 1) -tuples_on (Y /\ D)) \ (0 -tuples_on Y)) by COMPUT_1:5
.= (MultPlace f) .: ((m + 1) -tuples_on (Y /\ D)) by B2, 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 Z1;
hence (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous by Lm5, B0; :: 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) = (MultPlace f) .: {} by Z1
.= {} by RELAT_1:116 ;
hence (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous by Lm14; :: thesis: verum

end;

end;