let b be finite-support Function; :: thesis: dom (b * (canFS (support b))) = dom (canFS (support b))
A1: rng (canFS (support b)) c= support b by FINSEQ_1:def 4;
support b c= dom b by PRE_POLY:37;
then rng (canFS (support b)) c= dom b by A1;
hence dom (b * (canFS (support b))) = dom (canFS (support b)) by RELAT_1:27; :: thesis: verum