let X be set ; :: thesis: for l being Element of MapsC X holds
( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )
let l be Element of MapsC X; :: thesis: ( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )
set i1 = id$ (dom l);
set i2 = id$ (cod l);
A1: ( (id$ (dom l)) `2 = id (union (dom l)) & dom (id$ (dom l)) = dom l ) by Th24;
A2: l `2 is Function of (union (dom l)),(union (cod l)) by Th21;
then A3: rng (l `2) c= union (cod l) by RELAT_1:def 19;
( union (cod l) <> {} or union (dom l) = {} ) by Th21;
then A4: dom (l `2) = union (dom l) by A2, FUNCT_2:def 1;
A5: cod (id$ (dom l)) = dom l by Th24;
then A6: cod (l * (id$ (dom l))) = cod l by Th22;
( (l * (id$ (dom l))) `2 = (l `2) * ((id$ (dom l)) `2) & dom (l * (id$ (dom l))) = dom (id$ (dom l)) ) by A5, Th22;
hence l * (id$ (dom l)) = l by A4, A1, A6, Lm1, RELAT_1:52; :: thesis: (id$ (cod l)) * l = l
A7: ( (id$ (cod l)) `2 = id (union (cod l)) & cod (id$ (cod l)) = cod l ) by Th24;
A8: dom (id$ (cod l)) = cod l by Th24;
then A9: cod ((id$ (cod l)) * l) = cod (id$ (cod l)) by Th22;
( ((id$ (cod l)) * l) `2 = ((id$ (cod l)) `2) * (l `2) & dom ((id$ (cod l)) * l) = dom l ) by A8, Th22;
hence (id$ (cod l)) * l = l by A3, A7, A9, Lm1, RELAT_1:53; :: thesis: verum