let X, Y, Z be set ; for f being Function of X,Y
for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
<:f,g:> is Function of X,[:Y,Z:]
let f be Function of X,Y; for g being Function of X,Z st ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) holds
<:f,g:> is Function of X,[:Y,Z:]
let g be Function of X,Z; ( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) implies <:f,g:> is Function of X,[:Y,Z:] )
assume A1:
( ( Y = {} implies X = {} ) & ( Z = {} implies X = {} ) )
; <:f,g:> is Function of X,[:Y,Z:]
per cases
not ( [:Y,Z:] = {} & not X = {} & not ( [:Y,Z:] = {} & X <> {} ) )
;
suppose
(
[:Y,Z:] = {} implies
X = {} )
;
<:f,g:> is Function of X,[:Y,Z:]
(
rng f c= Y &
rng g c= Z )
by RELAT_1:def 19;
then A2:
[:(rng f),(rng g):] c= [:Y,Z:]
by ZFMISC_1:96;
(
dom f = X &
dom g = X )
by A1, FUNCT_2:def 1;
then A3:
dom <:f,g:> = X
by Th50;
rng <:f,g:> c= [:(rng f),(rng g):]
by Th51;
then
rng <:f,g:> c= [:Y,Z:]
by A2;
hence
<:f,g:> is
Function of
X,
[:Y,Z:]
by A3, FUNCT_2:2;
verum end; end;