let n, i be Nat; :: thesis: for D being non empty set
for d being Element of D
for p being Element of n -tuples_on D
for l being Nat st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l
let D be non empty set ; :: thesis: for d being Element of D
for p being Element of n -tuples_on D
for l being Nat st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l
let d be Element of D; :: thesis: for p being Element of n -tuples_on D
for l being Nat st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l
let p be Element of n -tuples_on D; :: thesis: for l being Nat st l in (dom p) \ {i} holds
(p +* (i,d)) . l = p . l
let l be Nat; :: thesis: ( l in (dom p) \ {i} implies (p +* (i,d)) . l = p . l )
assume l in (dom p) \ {i} ; :: thesis: (p +* (i,d)) . l = p . l
then not l in {i} by XBOOLE_0:def 5;
then l <> i by TARSKI:def 1;
hence (p +* (i,d)) . l = p . l by FUNCT_7:32; :: thesis: verum