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 st i in Seg n holds
(p +* (i,d)) . i = d
let D be non empty set ; :: thesis: for d being Element of D
for p being Element of n -tuples_on D st i in Seg n holds
(p +* (i,d)) . i = d
let d be Element of D; :: thesis: for p being Element of n -tuples_on D st i in Seg n holds
(p +* (i,d)) . i = d
let p be Element of n -tuples_on D; :: thesis: ( i in Seg n implies (p +* (i,d)) . i = d )
Seg n = dom p by FINSEQ_2:124;
hence ( i in Seg n implies (p +* (i,d)) . i = d ) by FUNCT_7:31; :: thesis: verum