let X be set ; :: thesis: for C1, C2 being Element of CSp X
for f being Function of union C1, union C2 st ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds
{(f . x),(f . y)} in C2 ) holds
[[C1,C2],f] in MapsC X
let C1, C2 be Element of CSp X; :: thesis: for f being Function of union C1, union C2 st ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds
{(f . x),(f . y)} in C2 ) holds
[[C1,C2],f] in MapsC X
let f be Function of union C1, union C2; :: thesis: ( ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds
{(f . x),(f . y)} in C2 ) implies [[C1,C2],f] in MapsC X )
assume that
A1: ( union C2 = {} implies union C1 = {} ) and
A2: for x, y being set st {x,y} in C1 holds
{(f . x),(f . y)} in C2 ; :: thesis: [[C1,C2],f] in MapsC X
reconsider f' = f as Element of FuncsC X by A1, Th17;
for x, y being set st {x,y} in C1 holds
{(f' . x),(f' . y)} in C2 by A2;
hence [[C1,C2],f] in MapsC X by A1; :: thesis: verum