let K be Field; for a being Element of K holds Per <*<*a*>*> = a
let a be Element of K; Per <*<*a*>*> = a
set M = <*<*a*>*>;
A1:
(PPath_product <*<*a*>*>) . (idseq 1) = a
proof
reconsider p =
idseq 1 as
Element of
Permutations 1
by MATRIX_2:def 11;
A2:
len (Path_matrix p,<*<*a*>*>) = 1
by MATRIX_3:def 7;
then A3:
dom (Path_matrix p,<*<*a*>*>) = Seg 1
by FINSEQ_1:def 3;
then A4:
1
in dom (Path_matrix p,<*<*a*>*>)
;
then
1
= p . 1
by A3, FUNCT_1:35;
then
(Path_matrix p,<*<*a*>*>) . 1
= <*<*a*>*> * 1,1
by A4, MATRIX_3:def 7;
then
(Path_matrix p,<*<*a*>*>) . 1
= a
by MATRIX_2:5;
then A5:
Path_matrix p,
<*<*a*>*> = <*a*>
by A2, FINSEQ_1:57;
(
(PPath_product <*<*a*>*>) . p = the
multF of
K $$ (Path_matrix p,<*<*a*>*>) &
<*a*> = 1
|-> a )
by Def1, FINSEQ_2:73;
hence
(PPath_product <*<*a*>*>) . (idseq 1) = a
by A5, FINSOP_1:17;
verum
end;
( FinOmega (Permutations 1) = {(idseq 1)} & idseq 1 in Permutations 1 )
by MATRIX_2:21, MATRIX_2:def 17, TARSKI:def 1;
hence
Per <*<*a*>*> = a
by A1, SETWISEO:26; verum