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

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; :: thesis: verum

let a be Element of K; :: thesis: Per <*<*a*>*> = a

set M = <*<*a*>*>;

A1: (PPath_product <*<*a*>*>) . (idseq 1) = a

proof

Permutations 1 in Fin (Permutations 1)
by FINSUB_1:def 5;
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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum