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