let X be set ; :: thesis: for m being Element of MapsT X holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
let m be Element of MapsT X; :: thesis: ( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
set i1 = id$ (dom m);
set i2 = id$ (cod m);
A1: m `2 is Function of ((dom m) `2),((cod m) `2) by Th42;
then A2: rng (m `2) c= (cod m) `2 by RELAT_1:def 19;
( (cod m) `2 <> {} or (dom m) `2 = {} ) by Th42;
then A3: dom (m `2) = (dom m) `2 by A1, FUNCT_2:def 1;
A4: cod (id$ (dom m)) = dom m ;
then A5: cod (m * (id$ (dom m))) = cod m by Th43;
( (m * (id$ (dom m))) `2 = (m `2) * ((id$ (dom m)) `2) & dom (m * (id$ (dom m))) = dom (id$ (dom m)) ) by A4, Th43;
hence m * (id$ (dom m)) = m by A3, A5, Lm4, RELAT_1:52; :: thesis: (id$ (cod m)) * m = m
A6: dom (id$ (cod m)) = cod m ;
then A7: cod ((id$ (cod m)) * m) = cod (id$ (cod m)) by Th43;
( ((id$ (cod m)) * m) `2 = ((id$ (cod m)) `2) * (m `2) & dom ((id$ (cod m)) * m) = dom m ) by A6, Th43;
hence (id$ (cod m)) * m = m by A2, A7, Lm4, RELAT_1:53; :: thesis: verum