set cS = canFS I;

set f = b * (canFS I);

A1: rng (b * (canFS I)) c= the carrier of G ;

( I = dom b & rng (canFS I) = I ) by FUNCT_2:def 3, PARTFUN1:def 2;

then dom (b * (canFS I)) = dom (canFS I) by RELAT_1:27;

then dom (b * (canFS I)) = Seg (len (canFS I)) by FINSEQ_1:def 3;

then b * (canFS I) is FinSequence by FINSEQ_1:def 2;

then reconsider f = b * (canFS I) as FinSequence of G by A1, FINSEQ_1:def 4;

take Product f ; :: thesis: ex f being FinSequence of G st

( Product f = Product f & f = b * (canFS I) )

thus ex f being FinSequence of G st

( Product f = Product f & f = b * (canFS I) ) ; :: thesis: verum

set f = b * (canFS I);

A1: rng (b * (canFS I)) c= the carrier of G ;

( I = dom b & rng (canFS I) = I ) by FUNCT_2:def 3, PARTFUN1:def 2;

then dom (b * (canFS I)) = dom (canFS I) by RELAT_1:27;

then dom (b * (canFS I)) = Seg (len (canFS I)) by FINSEQ_1:def 3;

then b * (canFS I) is FinSequence by FINSEQ_1:def 2;

then reconsider f = b * (canFS I) as FinSequence of G by A1, FINSEQ_1:def 4;

take Product f ; :: thesis: ex f being FinSequence of G st

( Product f = Product f & f = b * (canFS I) )

thus ex f being FinSequence of G st

( Product f = Product f & f = b * (canFS I) ) ; :: thesis: verum