let G be non empty multMagma ; :: thesis: for I being non empty finite set
for b being b₁ -defined the carrier of G -valued total Function holds
( b * (canFS I) is FinSequence of G & dom (b * (canFS I)) = Seg (card I) )
let I be non empty finite set ; :: thesis: for b being I -defined the carrier of G -valued total Function holds
( b * (canFS I) is FinSequence of G & dom (b * (canFS I)) = Seg (card I) )
let b be I -defined the carrier of G -valued total Function; :: thesis: ( b * (canFS I) is FinSequence of G & dom (b * (canFS I)) = Seg (card I) )
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 A2: 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;
len (canFS I) = card I by FINSEQ_1:93;
then dom f = Seg (card I) by A2, FINSEQ_1:def 3;
hence ( b * (canFS I) is FinSequence of G & dom (b * (canFS I)) = Seg (card I) ) ; :: thesis: verum