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