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_1:def 12;
dom qf = Seg n by A2, FUNCT_2:def 1;
then A3: (ITP ") * ITP = id (Seg n) by FUNCT_1:39;
ITP is Permutation of (Seg n) by MATRIX_1:def 12;
then rng qf = Seg n by FUNCT_2:def 3;
then A4: ITP * (ITP ") = id (Seg n) by FUNCT_1:39;
reconsider pf = ITP " as Element of (Group_of_Perm n) by MATRIX_1:def 13;
A5: ( idseq n = 1_ (Group_of_Perm n) & ITG * pf = the multF of (Group_of_Perm n) . (ITG,pf) ) by MATRIX_1:15;
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_1:def 13;
hence ITP " = ITG " by A3, A4, A5, A6, GROUP_1:def 5; :: thesis: verum