let D be non empty set ; :: thesis: for f being non empty FinSequence of D
for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f)
let f be non empty FinSequence of D; :: thesis: for g being FinSequence of D holds (g ^ f) /. (len (g ^ f)) = f /. (len f)
let g be FinSequence of D; :: thesis: (g ^ f) /. (len (g ^ f)) = f /. (len f)
A1: len f >= 1 by NAT_1:14;
len (g ^ f) = (len g) + (len f) by FINSEQ_1:22;
hence (g ^ f) /. (len (g ^ f)) = f /. (len f) by A1, SEQ_4:136; :: thesis: verum