deffunc H₁( SortSymbol of F₁()) -> Element of proj2 the Sorts of F₃() = the Sorts of F₃() . $1;
deffunc H₂( object , object ) -> Element of F₄() = F₅($2);
consider f being ManySortedFunction of the carrier of F₁() such that
A1: for o being SortSymbol of F₁() holds
( dom (f . o) = H₁(o) & ( for x being Element of H₁(o) holds (f . o) . x = H₂(o,x) ) ) from MSAFREE4:sch 7();
f is ManySortedFunction of F₃(),F₄()

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in the carrier of F₁() or f . i is Element of bool [:( the Sorts of F₃() . i),( the Sorts of F₄() . i):] )
assume i in the carrier of F₁() ; :: thesis: f . i is Element of bool [:( the Sorts of F₃() . i),( the Sorts of F₄() . i):]
then reconsider s = i as SortSymbol of F₁() ;
A2: dom (f . s) = H₁(s) by A1;
rng (f . s) c= the Sorts of F₄() . s

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (f . s) or a in the Sorts of F₄() . s )
assume a in rng (f . s) ; :: thesis: a in the Sorts of F₄() . s
then consider b being object such that
A3: ( b in H₁(s) & a = (f . s) . b ) by A2, FUNCT_1:def 3;
reconsider b = b as Element of H₁(s) by A3;
( s = the_sort_of b & the_sort_of b = the_sort_of F₅(b) & H₂(s,b) = (f . s) . b ) by A0, A1, SORT;
hence a in the Sorts of F₄() . s by A3, SORT; :: thesis: verum

end;

hence f . i is Function of ( the Sorts of F₃() . i),( the Sorts of F₄() . i) by A2, FUNCT_2:2; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of F₃(),F₄() ;
take f ; :: thesis: for t being Element of F₃() holds f . t = F₅(t)
let t be Element of F₃(); :: thesis: f . t = F₅(t)
A4: t in the Sorts of F₃() . (the_sort_of t) by SORT;
thus f . t = (f . (the_sort_of t)) . t by ABBR
.= F₅(t) by A1, A4 ; :: thesis: verum