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 9;
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:18;
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:40;
(
(PPath_product <*<*a*>*>) . p = the
multF of
K $$ (Path_matrix (p,<*<*a*>*>)) &
<*a*> = 1
|-> a )
by Def1, FINSEQ_2:59;
hence
(PPath_product <*<*a*>*>) . (idseq 1) = a
by A5, FINSOP_1:16;
verum
end;
( FinOmega (Permutations 1) = {(idseq 1)} & idseq 1 in Permutations 1 )
by MATRIX_2:19, MATRIX_2:def 14, TARSKI:def 1;
hence
Per <*<*a*>*> = a
by A1, SETWISEO:17; verum