let K be Field; :: thesis: for a being Element of K holds Per <*<*a*>*> = a
let a be Element of K; :: thesis: 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;
A6:
(PPath_product <*<*a*>*>) . p = the
multF of
K $$ (Path_matrix p,<*<*a*>*>)
by Def1;
<*a*> = 1
|-> a
by FINSEQ_2:73;
hence
(PPath_product <*<*a*>*>) . (idseq 1) = a
by A5, A6, FINSOP_1:17;
:: thesis: verum
end;
A7:
FinOmega (Permutations 1) = {(idseq 1)}
by MATRIX_2:21, MATRIX_2:def 17;
idseq 1 in Permutations 1
by MATRIX_2:21, TARSKI:def 1;
hence
Per <*<*a*>*> = a
by A1, A7, SETWISEO:26; :: thesis: verum