take id V ; :: thesis: ( dom (id V) = NAT & ( for n being Element of NAT holds (id V) . n is Permutation of (V . n) ) )
thus dom (id V) = NAT by PARTFUN1:def 2; :: thesis: for n being Element of NAT holds (id V) . n is Permutation of (V . n)
let n be Element of NAT ; :: thesis: (id V) . n is Permutation of (V . n)
(id V) . n = id (V . n) by MSUALG_3:def 1;
hence (id V) . n is Permutation of (V . n) ; :: thesis: verum