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: ( (id$ (dom m)) `2 = id ((dom m) `2) & dom (id$ (dom m)) = dom m ) by Th47;
A2: m `2 is Function of ((dom m) `2),((cod m) `2) by Th44;
then A3: rng (m `2) c= (cod m) `2 by RELAT_1:def 19;
( (cod m) `2 <> {} or (dom m) `2 = {} ) by Th44;
then A4: dom (m `2) = (dom m) `2 by A2, FUNCT_2:def 1;
A5: cod (id$ (dom m)) = dom m by Th47;
then A6: cod (m * (id$ (dom m))) = cod m by Th45;
( (m * (id$ (dom m))) `2 = (m `2) * ((id$ (dom m)) `2) & dom (m * (id$ (dom m))) = dom (id$ (dom m)) ) by A5, Th45;
hence m * (id$ (dom m)) = m by A4, A1, A6, Lm3, RELAT_1:52; :: thesis: (id$ (cod m)) * m = m
A7: ( (id$ (cod m)) `2 = id ((cod m) `2) & cod (id$ (cod m)) = cod m ) by Th47;
A8: dom (id$ (cod m)) = cod m by Th47;
then A9: cod ((id$ (cod m)) * m) = cod (id$ (cod m)) by Th45;
( ((id$ (cod m)) * m) `2 = ((id$ (cod m)) `2) * (m `2) & dom ((id$ (cod m)) * m) = dom m ) by A8, Th45;
hence (id$ (cod m)) * m = m by A3, A7, A9, Lm3, RELAT_1:53; :: thesis: verum