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