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

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