let D be non empty set ; :: thesis: for f1 being non empty FinSequence of D
for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1
let f1 be non empty FinSequence of D; :: thesis: for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1
let f2 be FinSequence of D; :: thesis: (f1 ^' f2) /. 1 = f1 /. 1
A1: 1 in dom f1 by FINSEQ_5:6;
1 in dom (f1 ^ ((2,(len f2)) -cut f2)) by FINSEQ_5:6;
hence (f1 ^' f2) /. 1 = (f1 ^ ((2,(len f2)) -cut f2)) . 1 by PARTFUN1:def 6
.= f1 . 1 by A1, FINSEQ_1:def 7
.= f1 /. 1 by A1, PARTFUN1:def 6 ;
:: thesis: verum