let A be finite set ; :: thesis: for B being non empty set
for f being A -defined b₁ -valued total Function holds f * (canFS A) is FinSequence of B
let B be non empty set ; :: thesis: for f being A -defined B -valued total Function holds f * (canFS A) is FinSequence of B
let f be A -defined B -valued total Function; :: thesis: f * (canFS A) is FinSequence of B
A1: rng (f * (canFS A)) c= B ;
( A = dom f & rng (canFS A) = A ) by FUNCT_2:def 3, PARTFUN1:def 2;
then dom (f * (canFS A)) = dom (canFS A) by RELAT_1:27;
then dom (f * (canFS A)) = Seg (len (canFS A)) by FINSEQ_1:def 3;
then f * (canFS A) is FinSequence by FINSEQ_1:def 2;
hence f * (canFS A) is FinSequence of B by A1, FINSEQ_1:def 4; :: thesis: verum