deffunc H1( SortSymbol of F1()) -> Element of proj2 the Sorts of F3() = the Sorts of F3() . $1;
deffunc H2( object , object ) -> Element of F4() = F5($2);
consider f being ManySortedFunction of the carrier of F1() such that
A1: for o being SortSymbol of F1() holds
( dom (f . o) = H1(o) & ( for x being Element of H1(o) holds (f . o) . x = H2(o,x) ) ) from MSAFREE4:sch 7();
 f is ManySortedFunction of F3(),F4()
proof
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in the carrier of F1() or f . i is Element of bool [:( the Sorts of F3() . i),( the Sorts of F4() . i):] )
assume i in the carrier of F1() ; :: thesis: f . i is Element of bool [:( the Sorts of F3() . i),( the Sorts of F4() . i):]
then reconsider s = i as SortSymbol of F1() ;
A2: dom (f . s) = H1(s) by A1;
rng (f . s) c= the Sorts of F4() . s
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (f . s) or a in the Sorts of F4() . s )
assume a in rng (f . s) ; :: thesis: a in the Sorts of F4() . s
then consider b being object such that
A3: ( b in H1(s) & a = (f . s) . b ) by A2, FUNCT_1:def 3;
reconsider b = b as Element of H1(s) by A3;
( s = the_sort_of b & the_sort_of b = the_sort_of F5(b) & H2(s,b) = (f . s) . b ) by A0, A1, SORT;
hence a in the Sorts of F4() . s by A3, SORT; :: thesis: verum
end;
hence f . i is Function of ( the Sorts of F3() . i),( the Sorts of F4() . i) by A2, FUNCT_2:2; :: thesis: verum
end;
then reconsider f = f as ManySortedFunction of F3(),F4() ;
take f ; :: thesis: for t being Element of F3() holds f . t = F5(t)
let t be Element of F3(); :: thesis: f . t = F5(t)
A4: t in the Sorts of F3() . (the_sort_of t) by SORT;
thus f . t = (f . (the_sort_of t)) . t by ABBR
.= F5(t) by A1, A4 ; :: thesis: verum