let m be CR_Sequence; :: thesis: for X being Group-Sequence st len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) holds
card the carrier of (product X) = Product m
let X be Group-Sequence; :: thesis: ( len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) implies card the carrier of (product X) = Product m )
assume A1: ( len m = len X & ( for i being Element of NAT st i in dom X holds
ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) ) ) ; :: thesis: card the carrier of (product X) = Product m
A2: dom (carr X) = Seg (len (carr X)) by FINSEQ_1:def 3
.= Seg (len X) by PRVECT_1:def 11
.= dom X by FINSEQ_1:def 3 ;
A3: dom X = Seg (len X) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3, A1 ;
A4: for i being Element of NAT st i in dom (carr X) holds
card ((carr X) . i) = m . i

proof

let i be Element of NAT ; :: thesis: ( i in dom (carr X) implies card ((carr X) . i) = m . i )
assume A5: i in dom (carr X) ; :: thesis: card ((carr X) . i) = m . i
reconsider i0 = i as Element of dom X by A2, A5;
consider mi being non zero Nat such that
A6: ( mi = m . i & X . i = Z/Z mi ) by A2, A5, A1;
thus card ((carr X) . i) = card the carrier of (X . i0) by PRVECT_1:def 11
.= m . i by A6 ; :: thesis: verum

end;

A7: len (carr X) = len m by A1, PRVECT_1:def 11;

now :: thesis: for i being Nat st i in dom m holds
m . i in NAT

let i be Nat; :: thesis: ( i in dom m implies m . i in NAT )
assume i in dom m ; :: thesis: m . i in NAT
then ex mi being non zero Nat st
( mi = m . i & X . i = Z/Z mi ) by A3, A1;
hence m . i in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then m is FinSequence of NAT by FINSEQ_2:12;
hence card the carrier of (product X) = Product m by A4, A7, Th18; :: thesis: verum