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:13; :: thesis: ( not i in dom p implies ([#] (p,d)) . i = d )
A1: i in NAT by ORDINAL1:def 12;
assume not i in dom p ; :: thesis: ([#] (p,d)) . i = d
hence ([#] (p,d)) . i = (NAT --> d) . i by FUNCT_4:11
.= d by A1, FUNCOP_1:7 ;
:: thesis: verum