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

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