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