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