let k, n be Nat; :: thesis: for b being ManySortedSet of n st k <= n holds
(0,k) -cut b = b | k
let b be ManySortedSet of n; :: thesis: ( k <= n implies (0,k) -cut b = b | k )
assume k <= n ; :: thesis: (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

proof

let x be object ; :: thesis: ( x in k implies ((0,k) -cut b) . x = (b | k) . x )
assume A4: x in k ; :: thesis: ((0,k) -cut b) . x = (b | k) . x
then x in Segm k ;
then reconsider n = x as Element of NAT ;
thus ((0,k) -cut b) . x = b . (0 + n) by A4, A3, BAGORDER:def 1
.= (b | k) . x by A4, FUNCT_1:49 ; :: thesis: verum

end;

hence (0,k) -cut b = b | k by FUNCT_1:2, A2, A3; :: thesis: verum