A1:
for x being object st x in F_{1}() holds

F_{3}(x) in F_{2}()
;

consider IT being Function of F_{1}(),F_{2}() such that

A2: for x being object st x in F_{1}() holds

IT . x = F_{3}(x)
from FUNCT_2:sch 2(A1);

take IT ; :: thesis: for x being set st x in F_{1}() holds

IT /. x = F_{3}(x)

let x be set ; :: thesis: ( x in F_{1}() implies IT /. x = F_{3}(x) )

assume A3: x in F_{1}()
; :: thesis: IT /. x = F_{3}(x)

hence F_{3}(x) =
IT . x
by A2

.= IT /. x by A3, FUNCT_2:def 13 ;

:: thesis: verum

F

consider IT being Function of F

A2: for x being object st x in F

IT . x = F

take IT ; :: thesis: for x being set st x in F

IT /. x = F

let x be set ; :: thesis: ( x in F

assume A3: x in F

hence F

.= IT /. x by A3, FUNCT_2:def 13 ;

:: thesis: verum