let V be non empty set ; :: thesis: for m being Element of Maps V holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
let m be Element of Maps V; :: 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) & dom (id$ (dom m)) = dom m ) by Th11;
A2: m `2 is Function of (dom m),(cod m) by Th9;
then A3: rng (m `2) c= cod m by RELAT_1:def 19;
( cod m <> {} or dom m = {} ) by Th9;
then A4: dom (m `2) = dom m by A2, FUNCT_2:def 1;
A5: cod (id$ (dom m)) = dom m by Th11;
then A6: cod (m * (id$ (dom m))) = cod m by Th12;
( (m * (id$ (dom m))) `2 = (m `2) * ((id$ (dom m)) `2) & dom (m * (id$ (dom m))) = dom (id$ (dom m)) ) by A5, Th12;
hence m * (id$ (dom m)) = m by A4, A1, A6, Lm2, RELAT_1:52; :: thesis: (id$ (cod m)) * m = m
A7: ( (id$ (cod m)) `2 = id (cod m) & cod (id$ (cod m)) = cod m ) by Th11;
A8: dom (id$ (cod m)) = cod m by Th11;
then A9: cod ((id$ (cod m)) * m) = cod (id$ (cod m)) by Th12;
( ((id$ (cod m)) * m) `2 = ((id$ (cod m)) `2) * (m `2) & dom ((id$ (cod m)) * m) = dom m ) by A8, Th12;
hence (id$ (cod m)) * m = m by A3, A7, A9, Lm2, RELAT_1:53; :: thesis: verum