deffunc H₁( Element of (product F)) -> set = $1 * a;
consider f being Function such that
A1: dom f = [#] (product F) and
A2: for x being Element of (product F) st x in [#] (product F) holds
f . x = H₁(x) from GROUP_21:sch 1();

now :: thesis: for y being object st y in rng f holds
y in [#] (product (F * a))

let y be object ; :: thesis: ( y in rng f implies y in [#] (product (F * a)) )
assume y in rng f ; :: thesis: y in [#] (product (F * a))
then consider x being object such that
A3: x in dom f and
A4: f . x = y by FUNCT_1:def 3;
reconsider x = x as Element of (product F) by A1, A3;
x * a in product (F * a) by Th1;
hence y in [#] (product (F * a)) by A2, A4; :: thesis: verum

end;

then rng f c= [#] (product (F * a)) ;
then reconsider f = f as Function of (product F),(product (F * a)) by A1, FUNCT_2:2;
take f ; :: thesis: for x being Element of (product F) holds f . x = x * a
thus for x being Element of (product F) holds f . x = x * a by A2; :: thesis: verum