let X be set ; :: thesis: for T1, T2 being Element of TOL X
for f being Function of (T1 `2),(T2 `2) st ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) holds
[[T1,T2],f] in MapsT X
let T1, T2 be Element of TOL X; :: thesis: for f being Function of (T1 `2),(T2 `2) st ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) holds
[[T1,T2],f] in MapsT X
let f be Function of (T1 `2),(T2 `2); :: thesis: ( ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) implies [[T1,T2],f] in MapsT X )
assume that
A1: ( T2 `2 = {} implies T1 `2 = {} ) and
A2: for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ; :: thesis: [[T1,T2],f] in MapsT X
reconsider f9 = f as Element of FuncsT X by A1, Th38;
for x, y being set st [x,y] in T1 `1 holds
[(f9 . x),(f9 . y)] in T2 `1 by A2;
hence [[T1,T2],f] in MapsT X by A1; :: thesis: verum