reconsider h = <%> D as 0 -element FinSequence ;
reconsider z = len h as zero Nat ;
reconsider k = len f as Nat ;
reconsider g = f as k -element FinSequence by CARD_1:def 7;
A1: dom ((<%> D) ^ f) = z + k by Def1;
A2: len f = len (FS2XFS f) by AFINSQ_1:def 8;
for l being Nat st l in dom (FS2XFS f) holds
((<%> D) ^ f) . l = (FS2XFS f) . l

proof

let l be Nat; :: thesis: ( l in dom (FS2XFS f) implies ((<%> D) ^ f) . l = (FS2XFS f) . l )
assume l in dom (FS2XFS f) ; :: thesis: ((<%> D) ^ f) . l = (FS2XFS f) . l
then B2: l in Segm (len f) by AFINSQ_1:def 8;
then B3: l < len f by NAT_1:44;
reconsider j = l + 1 as non zero Nat ;
( 1 <= j & j <= len f ) by B3, NAT_1:13, NAT_1:14;
then B4: j in dom f by FINSEQ_3:25;
(h ^ g) . l = (h ^ g) . ((z + j) - 1)
.= f . j by B4, Def1
.= (FS2XFS f) . l by B2, NAT_1:44, AFINSQ_1:def 8 ;
hence ((<%> D) ^ f) . l = (FS2XFS f) . l ; :: thesis: verum

end;

hence for b₁ being set holds
( b₁ = FS2XFS f iff b₁ = (<%> D) ^ f ) by A1, A2; :: thesis: verum