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

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