let S1, S2 be Series of X,L; :: 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
S1 . b = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies S1 . b = 0. L ) ) ) & ( 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
S2 . b = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies S2 . b = 0. L ) ) ) implies S1 = S2 )
set P = p `^ (t . x);
assume that
A5: 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
S1 . b = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies S1 . b = 0. L ) ) and
A6: 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
S2 . b = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies S2 . b = 0. L ) ) ; :: thesis: S1 = S2
for x being object st x in Bags X holds
S1 . x = S2 . x

proof

let b be object ; :: thesis: ( b in Bags X implies S1 . b = S2 . b )
assume A7: b in Bags X ; :: thesis: S1 . b = S2 . b
reconsider b = b as Element of Bags X by A7;

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: S1 . b = S2 . b

then consider s being bag of X such that
A8: b = Subst (t,x,s) ;
( S1 . b = (p `^ (t . x)) . s & (p `^ (t . x)) . s = S2 . b ) by A8, A5, A6;
hence S1 . b = S2 . b ; :: thesis: verum

end;

suppose for s being bag of X holds b <> Subst (t,x,s) ; :: thesis: S1 . b = S2 . b

then ( S1 . b = 0. L & 0. L = S2 . b ) by A5, A6;
hence S1 . b = S2 . b ; :: thesis: verum

end;

end;

end;

hence S1 = S2 ; :: thesis: verum