let c be Complex; :: thesis: XFS2FS <%c%> = <*c*>
A1: len (XFS2FS <%c%>) = len <%c%> by AFINSQ_1:def 9;
A2: len <%c%> = 1 by AFINSQ_1:def 4;
then A3: ( dom (XFS2FS <%c%>) = Seg 1 & dom <*c*> = Seg 1 ) by A1, FINSEQ_1:def 3, FINSEQ_1:def 8;
for k being Nat st k in dom <*c*> holds
(XFS2FS <%c%>) . k = <*c*> . k

proof

let k be Nat; :: thesis: ( k in dom <*c*> implies (XFS2FS <%c%>) . k = <*c*> . k )
assume k in dom <*c*> ; :: thesis: (XFS2FS <%c%>) . k = <*c*> . k
then k in Seg 1 by FINSEQ_1:def 8;
then ( 1 <= k & k <= 1 ) by FINSEQ_1:1;
then B3: k = 1 by XXREAL_0:1;
then <*c*> . k = <%c%> . 0
.= <%c%> . (1 - 1)
.= (XFS2FS <%c%>) . k by A2, B3, AFINSQ_1:def 9 ;
hence (XFS2FS <%c%>) . k = <*c*> . k ; :: thesis: verum

end;

hence XFS2FS <%c%> = <*c*> by A3; :: thesis: verum