let X be set ; :: thesis: for l, l1 being Element of MapsC X st l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 holds
l = l1
let l, l1 be Element of MapsC X; :: thesis: ( l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 implies l = l1 )
l = [[(dom l),(cod l)],(l `2)] by Th20;
hence ( l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 implies l = l1 ) by Th20; :: thesis: verum