let D be non empty set ; :: thesis: for f1, f2 being FinSequence of D st f1 <> {} holds
(f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2
let f1, f2 be FinSequence of D; :: thesis: ( f1 <> {} implies (f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2 )
assume f1 <> {} ; :: thesis: (f1 ^ f2) /^ 1 = (f1 /^ 1) ^ f2
then consider p being Element of D, df1 being FinSequence of D such that
p = f1 . 1 and
A1: f1 = <*p*> ^ df1 by FINSEQ_3:102;
thus (f1 ^ f2) /^ 1 = (<*p*> ^ (df1 ^ f2)) /^ 1 by A1, FINSEQ_1:32
.= df1 ^ f2 by Th45
.= (f1 /^ 1) ^ f2 by A1, Th45 ; :: thesis: verum