let k be Nat; :: thesis: for E being non empty set
for p, q being FinSequence of E st k in dom p holds
(p ^ q) /. k = p /. k
let E be non empty set ; :: thesis: for p, q being FinSequence of E st k in dom p holds
(p ^ q) /. k = p /. k
let p, q be FinSequence of E; :: thesis: ( k in dom p implies (p ^ q) /. k = p /. k )
assume A1: k in dom p ; :: thesis: (p ^ q) /. k = p /. k
then k in dom (p ^ q) by FINSEQ_3:22;
hence (p ^ q) /. k = (p ^ q) . k by PARTFUN1:def 6
.= p . k by A1, FINSEQ_1:def 7
.= p /. k by A1, PARTFUN1:def 6 ;
:: thesis: verum