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

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