set p = l * (canFS ((T " {w}) /\ (Carrier l)));
set f = canFS ((T " {w}) /\ (Carrier l));
dom l = the carrier of V by FUNCT_2:def 1;
then rng (canFS ((T " {w}) /\ (Carrier l))) c= dom l by XBOOLE_1:1;
hence l * (canFS ((T " {w}) /\ (Carrier l))) is the carrier of K -valued FinSequence by FINSEQ_1:16; :: thesis: verum