deffunc H₁( Element of Bags n) -> Element of the carrier of L = (p . $1) + (q . $1);
consider f being Function of (Bags n),the carrier of L such that
A1: for x being Element of Bags n holds f . x = H₁(x) from FUNCT_2:sch 4();
reconsider f = f as Function of (Bags n),L ;
reconsider f = f as Series of n,L ;
take f ; :: thesis: for x being bag of n holds f . x = (p . x) + (q . x)
let x be bag of n; :: thesis: f . x = (p . x) + (q . x)
x in Bags n by PRE_POLY:def 12;
hence f . x = (p . x) + (q . x) by A1; :: thesis: verum