set P = p `^ (t . x);
defpred S<sub>1</sub>[ Element of Bags X, Element of L] means ( ( ex s being bag of X st $1 = Subst (t,x,s) implies for s being bag of X st $1 = Subst (t,x,s) holds
$2 = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds $1 <> Subst (t,x,s) ) implies $2 = 0. L ) );
A1: for x being Element of Bags X ex y being Element of L st S₁[x,y]

proof

let b be Element of Bags X; :: thesis: ex y being Element of L st S₁[b,y]

per cases ( ex s being bag of X st b = Subst (t,x,s) or for s being bag of X holds b <> Subst (t,x,s) ) ;

suppose ex s being bag of X st b = Subst (t,x,s) ; :: thesis: ex y being Element of L st S₁[b,y]

then consider s being bag of X such that
A2: b = Subst (t,x,s) ;
take M = (p `^ (t . x)) . s; :: thesis: S₁[b,M]
thus S₁[b,M] by A2, Th32; :: thesis: verum

end;

suppose A3: for s being bag of X holds b <> Subst (t,x,s) ; :: thesis: ex y being Element of L st S₁[b,y]

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

end;

end;

end;

consider S being Function of (Bags X),L such that
A4: for x being Element of Bags X holds S₁[x,S . x] from FUNCT_2:sch 3(A1);
take S ; :: thesis: for b being bag of X holds
( ( ex s being bag of X st b = Subst (t,x,s) implies for s being bag of X st b = Subst (t,x,s) holds
S . b = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies S . b = 0. L ) )
let b be bag of X; :: thesis: ( ( ex s being bag of X st b = Subst (t,x,s) implies for s being bag of X st b = Subst (t,x,s) holds
S . b = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies S . b = 0. L ) )
reconsider bb = b as Element of Bags X by PRE_POLY:def 12;
thus ( ex s being bag of X st b = Subst (t,x,s) implies for s being bag of X st b = Subst (t,x,s) holds
S . b = (p `^ (t . x)) . s ) :: thesis: ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies S . b = 0. L )

proof

assume ex s being bag of X st b = Subst (t,x,s) ; :: thesis: for s being bag of X st b = Subst (t,x,s) holds
S . b = (p `^ (t . x)) . s
let s be bag of X; :: thesis: ( b = Subst (t,x,s) implies S . b = (p `^ (t . x)) . s )
assume b = Subst (t,x,s) ; :: thesis: S . b = (p `^ (t . x)) . s
then S . bb = (p `^ (t . x)) . s by A4;
hence S . b = (p `^ (t . x)) . s ; :: thesis: verum

end;

S₁[bb,S . bb] by A4;
hence ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies S . b = 0. L ) ; :: thesis: verum