let G be Group; :: thesis: for F1, F2 being FinSequence of the carrier of G st G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 holds
Product F1 = Product F2
let F1, F2 be FinSequence of the carrier of G; :: thesis: ( G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 implies Product F1 = Product F2 )
set g = the multF of G;
A1: the multF of G is associative by GROUP_1:31;
assume G is commutative Group ; :: thesis: ( not F1 is one-to-one or not F2 is one-to-one or not rng F1 = rng F2 or Product F1 = Product F2 )
then A2: the multF of G is commutative by GROUP_3:2;
assume ( F1 is one-to-one & F2 is one-to-one & rng F1 = rng F2 ) ; :: thesis: Product F1 = Product F2
hence Product F1 = Product F2 by A2, A1, FINSOP_1:9, GROUP_1:34; :: thesis: verum