let G be non empty multMagma ; :: thesis: for I being non empty finite set

for b being b_{1} -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

for b being b

( 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