let X be set ; for l being Element of MapsC X holds
( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l ) )
let l be Element of MapsC X; ( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l ) )
consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that
A1:
l = [[C1,C2],g]
and
A2:
( ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) )
and
A3:
for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2
by Th18;
A4:
C2 = cod l
by A1;
A5:
( g = l `2 & C1 = dom l )
by A1;
thus
( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) )
by A1, A2; for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l
let x, y be set ; ( {x,y} in dom l implies {((l `2) . x),((l `2) . y)} in cod l )
assume
{x,y} in dom l
; {((l `2) . x),((l `2) . y)} in cod l
hence
{((l `2) . x),((l `2) . y)} in cod l
by A3, A5, A4; verum