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