let n be Nat; :: thesis: for D being non empty set

for d being Element of D

for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

let D be non empty set ; :: thesis: for d being Element of D

for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

let d be Element of D; :: thesis: for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

let z be Tuple of n,D; :: thesis: (z ^ <*d*>) /. (n + 1) = d

len <*d*> = 1 by FINSEQ_1:39;

then 0 + 1 in Seg (len <*d*>) ;

then A1: 0 + 1 in dom <*d*> by FINSEQ_1:def 3;

len z = n by CARD_1:def 7;

hence (z ^ <*d*>) /. (n + 1) = <*d*> /. 1 by A1, FINSEQ_4:69

.= d by FINSEQ_4:16 ;

:: thesis: verum

for d being Element of D

for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

let D be non empty set ; :: thesis: for d being Element of D

for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

let d be Element of D; :: thesis: for z being Tuple of n,D holds (z ^ <*d*>) /. (n + 1) = d

let z be Tuple of n,D; :: thesis: (z ^ <*d*>) /. (n + 1) = d

len <*d*> = 1 by FINSEQ_1:39;

then 0 + 1 in Seg (len <*d*>) ;

then A1: 0 + 1 in dom <*d*> by FINSEQ_1:def 3;

len z = n by CARD_1:def 7;

hence (z ^ <*d*>) /. (n + 1) = <*d*> /. 1 by A1, FINSEQ_4:69

.= d by FINSEQ_4:16 ;

:: thesis: verum