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

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