let n be Nat; :: thesis: for ITP being Element of Permutations n
for ITG being Element of (Group_of_Perm n) st ITG = ITP & n >= 1 holds
ITP " = ITG "
let ITP be Element of Permutations n; :: thesis: for ITG being Element of (Group_of_Perm n) st ITG = ITP & n >= 1 holds
ITP " = ITG "
let ITG be Element of (Group_of_Perm n); :: thesis: ( ITG = ITP & n >= 1 implies ITP " = ITG " )
assume that
A1: ITG = ITP and
A2: n >= 1 ; :: thesis: ITP " = ITG "
reconsider qf = ITP as Function of (Seg n),(Seg n) by MATRIX_2:def 11;
dom qf = Seg n by A2, FUNCT_2:def 1;
then A3: (ITP " ) * ITP = id (Seg n) by FUNCT_1:61;
ITP is Permutation of (Seg n) by MATRIX_2:def 11;
then rng qf = Seg n by FUNCT_2:def 3;
then A4: ITP * (ITP " ) = id (Seg n) by FUNCT_1:61;
reconsider pf = ITP " as Element of (Group_of_Perm n) by MATRIX_2:def 13;
A5: ( idseq n = 1_ (Group_of_Perm n) & ITG * pf = the multF of (Group_of_Perm n) . ITG,pf ) by MATRIX_2:28;
A6: pf * ITG = the multF of (Group_of_Perm n) . pf,ITG ;
( the multF of (Group_of_Perm n) . ITG,pf = (ITP " ) * ITP & the multF of (Group_of_Perm n) . pf,ITG = ITP * (ITP " ) ) by A1, MATRIX_2:def 13;
hence ITP " = ITG " by A3, A4, A5, A6, GROUP_1:def 6; :: thesis: verum