let k, n be Nat; for b being ManySortedSet of n st k <= n holds
(0,k) -cut b = b | k
let b be ManySortedSet of n; ( k <= n implies (0,k) -cut b = b | k )
assume
k <= n
; (0,k) -cut b = b | k
then A1:
Segm k c= Segm n
by NAT_1:39;
A2:
dom (b | k) = k
by A1, PARTFUN1:def 2;
A3:
( dom ((0,k) -cut b) = k -' 0 & k -' 0 = k )
by NAT_D:40, PARTFUN1:def 2;
for x being object st x in k holds
((0,k) -cut b) . x = (b | k) . x
hence
(0,k) -cut b = b | k
by FUNCT_1:2, A2, A3; verum