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_1:def 12;
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_0:49;
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;
Permutations 1 in Fin (Permutations 1)
by FINSUB_1:def 5;
then
In ((Permutations 1),(Fin (Permutations 1))) = Permutations 1
by SUBSET_1:def 8;
then
( In ((Permutations 1),(Fin (Permutations 1))) = {(idseq 1)} & idseq 1 in Permutations 1 )
by MATRIX_1:10, TARSKI:def 1;
hence
Per <*<*a*>*> = a
by A1, SETWISEO:17; verum