let D be non empty set ; :: thesis: for d being Element of D
for i being Nat
for p being FinSequence of D holds
( ( i in dom p implies ([#] p,d) . i = p . i ) & ( not i in dom p implies ([#] p,d) . i = d ) )
let d be Element of D; :: thesis: for i being Nat
for p being FinSequence of D holds
( ( i in dom p implies ([#] p,d) . i = p . i ) & ( not i in dom p implies ([#] p,d) . i = d ) )
let i be Nat; :: thesis: for p being FinSequence of D holds
( ( i in dom p implies ([#] p,d) . i = p . i ) & ( not i in dom p implies ([#] p,d) . i = d ) )
let p be FinSequence of D; :: thesis: ( ( i in dom p implies ([#] p,d) . i = p . i ) & ( not i in dom p implies ([#] p,d) . i = d ) )
thus ( i in dom p implies ([#] p,d) . i = p . i ) by FUNCT_4:14; :: thesis: ( not i in dom p implies ([#] p,d) . i = d )
A1: i in NAT by ORDINAL1:def 13;
assume not i in dom p ; :: thesis: ([#] p,d) . i = d
hence ([#] p,d) . i = (NAT --> d) . i by FUNCT_4:12
.= d by A1, FUNCOP_1:13 ;
:: thesis: verum