let X be set ; :: thesis: for m being Element of MapsT X holds
( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1 ) )
let m be Element of MapsT X; :: thesis: ( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1 ) )
consider f being Element of FuncsT X, T1, T2 being Element of TOL X such that
A1: m = [[T1,T2],f] and
A2: ( ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) ) and
A3: for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 by Th41;
A4: m = [[(dom m),(cod m)],(m `2)] by Th43;
then A5: T2 = cod m by A1, Lm2;
A6: ( f = m `2 & T1 = dom m ) by A1, A4, Lm2, ZFMISC_1:27;
hence ( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) ) by A1, A2, A4, Lm2; :: thesis: for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1
let x, y be set ; :: thesis: ( [x,y] in (dom m) `1 implies [((m `2) . x),((m `2) . y)] in (cod m) `1 )
assume [x,y] in (dom m) `1 ; :: thesis: [((m `2) . x),((m `2) . y)] in (cod m) `1
hence [((m `2) . x),((m `2) . y)] in (cod m) `1 by A3, A6, A5; :: thesis: verum