( P₂[F₄()] & F₃() c= F₄() & ( for P being ManySortedRelation of F₂() st P₂[P] & F₃() c= P holds
F₄() c= P ) )

A1: for R being ManySortedRelation of F₂() holds
( P₂[R] iff for s1, s2 being SortSymbol of F₁()
for f being Function of ( the Sorts of F₂() . s1),( the Sorts of F₂() . s2) st P₁[f,s1,s2] holds
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) and
A2: for s1, s2, s3 being SortSymbol of F₁()
for f1 being Function of ( the Sorts of F₂() . s1),( the Sorts of F₂() . s2)
for f2 being Function of ( the Sorts of F₂() . s2),( the Sorts of F₂() . s3) st P₁[f1,s1,s2] & P₁[f2,s2,s3] holds
P₁[f2 * f1,s1,s3] and
A3: for s being SortSymbol of F₁() holds P₁[ id ( the Sorts of F₂() . s),s,s] and
A4: for s being SortSymbol of F₁()
for a, b being Element of F₂(),s holds
( [a,b] in F₄() . s iff ex s9 being SortSymbol of F₁() ex f being Function of ( the Sorts of F₂() . s9),( the Sorts of F₂() . s) ex x, y being Element of F₂(),s9 st
( P₁[f,s9,s] & [x,y] in F₃() . s9 & a = f . x & b = f . y ) )