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 XFinSequence by CARD_1:def 7;
A1: dom ((<*> D) ^ f) = Seg (len (h ^ g)) by FINSEQ_1:def 3
.= Seg (len f) by CARD_1:def 7 ;
A2: Seg (len f) = Seg (len (XFS2FS f)) by AFINSQ_1:def 9
.= dom (XFS2FS f) by FINSEQ_1:def 3 ;
for l being Nat st l in dom (XFS2FS f) holds
((<*> D) ^ f) . l = (XFS2FS f) . l

proof

let l be Nat; :: thesis: ( l in dom (XFS2FS f) implies ((<*> D) ^ f) . l = (XFS2FS f) . l )
assume B1: l in dom (XFS2FS f) ; :: thesis: ((<*> D) ^ f) . l = (XFS2FS f) . l
then B2: ( 1 <= l & l <= len f ) by A2, FINSEQ_1:1;
then reconsider j = l - 1 as Nat ;
j + 1 <= len f by A2, B1, FINSEQ_1:1;
then j < len f by NAT_1:13;
then B3: j in Segm (len f) by NAT_1:44;
(h ^ g) . l = (h ^ g) . ((z + j) + 1)
.= f . ((j + 1) -' 1) by B3, Def2
.= (XFS2FS f) . (j + 1) by B2, AFINSQ_1:def 9 ;
hence ((<*> D) ^ f) . l = (XFS2FS f) . l ; :: thesis: verum

end;

hence for b₁ being FinSequence of D holds
( b₁ = XFS2FS f iff b₁ = (<*> D) ^ f ) by A1, A2; :: thesis: verum