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

hence card the carrier of (product X) = Product m by A4, A7, Th18; :: thesis: verum

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

A7:
len (carr X) = len m
by A1, PRVECT_1:def 11;
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;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

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

m . i in NAT

then
m is FinSequence of NAT
by FINSEQ_2:12;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;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

hence card the carrier of (product X) = Product m by A4, A7, Th18; :: thesis: verum