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 f9 = f as Element of FuncsC X by A1, Th17;
for x, y being set st {x,y} in C1 holds
{(f9 . x),(f9 . y)} in C2 by A2;
hence [[C1,C2],f] in MapsC X by A1; :: thesis: verum