let V be SetValuation; :: thesis: for P being Permutation of V holds Perm (P,VERUM) = id (SetVal (V,VERUM))

let P be Permutation of V; :: thesis: Perm (P,VERUM) = id (SetVal (V,VERUM))

thus Perm (P,VERUM) = id 1 by Def5

.= id (SetVal (V,VERUM)) by Def2 ; :: thesis: verum

let P be Permutation of V; :: thesis: Perm (P,VERUM) = id (SetVal (V,VERUM))

thus Perm (P,VERUM) = id 1 by Def5

.= id (SetVal (V,VERUM)) by Def2 ; :: thesis: verum