defpred S₁[ Element of Bags (n + 1), Element of L] means ( ( $1 . n <> 0 implies $2 = 0. L ) & ( $1 . n = 0 implies $2 = p . ((0,n) -cut $1) ) );
A1: for x being Element of Bags (n + 1) ex y being Element of L st S₁[x,y]

proof

let x be Element of Bags (n + 1); :: thesis: ex y being Element of L st S₁[x,y]
n = n -' 0 by NAT_D:40;
then (0,n) -cut x in Bags n by PRE_POLY:def 12;
then A2: (0,n) -cut x in dom p by PARTFUN1:def 2;

per cases ( x . n <> 0 or x . n = 0 ) ;

suppose A3: x . n <> 0 ; :: thesis: ex y being Element of L st S₁[x,y]

take 0. L ; :: thesis: S₁[x, 0. L]
thus S₁[x, 0. L] by A3; :: thesis: verum

end;

suppose A4: x . n = 0 ; :: thesis: ex y being Element of L st S₁[x,y]

take p /. ((0,n) -cut x) ; :: thesis: S₁[x,p /. ((0,n) -cut x)]
thus S₁[x,p /. ((0,n) -cut x)] by A4, A2, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

consider f being Function of (Bags (n + 1)),L such that
A5: for x being Element of Bags (n + 1) holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for b being bag of n + 1 holds
( ( b . n <> 0 implies f . b = 0. L ) & ( b . n = 0 implies f . b = p . ((0,n) -cut b) ) )
let b be bag of n + 1; :: thesis: ( ( b . n <> 0 implies f . b = 0. L ) & ( b . n = 0 implies f . b = p . ((0,n) -cut b) ) )
b is Element of Bags (n + 1) by PRE_POLY:def 12;
hence ( ( b . n <> 0 implies f . b = 0. L ) & ( b . n = 0 implies f . b = p . ((0,n) -cut b) ) ) by A5; :: thesis: verum