A: ( rng (canFS (f " {v})) c= f " {v} & dom l = the carrier of U & dom f = B ) by FUNCT_2:def 1;

now :: thesis: for o being object st o in rng (canFS (f " {v})) holds
o in dom l

let o be object ; :: thesis: ( o in rng (canFS (f " {v})) implies o in dom l )
assume o in rng (canFS (f " {v})) ; :: thesis: o in dom l
then ( o in dom f & f . o in {v} ) by FUNCT_1:def 7;
hence o in dom l by A; :: thesis: verum

end;

then rng (canFS (f " {v})) c= dom l ;
then reconsider g = l * (canFS (f " {v})) as FinSequence by FINSEQ_1:16;

now :: thesis: for o being object st o in rng g holds
o in the carrier of F

let o be object ; :: thesis: ( o in rng g implies o in the carrier of F )
assume o in rng g ; :: thesis: o in the carrier of F
then o in rng l by FUNCT_1:14;
hence o in the carrier of F ; :: thesis: verum

end;

then rng g c= the carrier of F ;
hence l * (canFS (f " {v})) is FinSequence of the carrier of F by FINSEQ_1:def 4; :: thesis: verum