deffunc H₁( object ) -> object = F₄($1,(F₃() . $1));
consider f being Function such that
A1: dom f = F₁() and
A2: for a being object st a in F₁() holds
f . a = H₁(a) from FUNCT_1:sch 3();
reconsider f = f as ManySortedSet of F₁() by A1, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: for a being set
for b being Element of F₂() st a in F₁() & b = F₃() . a holds
f . a = F₄(a,b)
thus for a being set
for b being Element of F₂() st a in F₁() & b = F₃() . a holds
f . a = F₄(a,b) by A2; :: thesis: verum