let G be Group; :: thesis: for F1, F2 being FinSequence of the carrier of G st G is commutative Group holds
for P being Permutation of dom F1 st F2 = F1 * P holds
Product F1 = Product F2
let F1, F2 be FinSequence of the carrier of G; :: thesis: ( G is commutative Group implies for P being Permutation of dom F1 st F2 = F1 * P holds
Product F1 = Product F2 )
set g = the multF of G;
assume G is commutative Group ; :: thesis: for P being Permutation of dom F1 st F2 = F1 * P holds
Product F1 = Product F2
then A1: ( the multF of G is commutative & the multF of G is having_a_unity & the multF of G is associative ) by GROUP_1:31, GROUP_1:34, GROUP_3:2;
let P be Permutation of dom F1; :: thesis: ( F2 = F1 * P implies Product F1 = Product F2 )
assume F2 = F1 * P ; :: thesis: Product F1 = Product F2
hence Product F1 = Product F2 by A1, FINSOP_1:8; :: thesis: verum