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:33;
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