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 f' = f as Element of FuncsT X by A1, Th40;
for x, y being set st [x,y] in T1 `1 holds
[(f' . x),(f' . y)] in T2 `1 by A2;
hence [[T1,T2],f] in MapsT X by A1; :: thesis: verum