let X, Y, V, Z be set ; :: thesis: for f being Function of X,Y
for g being Function of V,Z holds [:f,g:] is Function of [:X,V:],[:Y,Z:]
let f be Function of X,Y; :: thesis: for g being Function of V,Z holds [:f,g:] is Function of [:X,V:],[:Y,Z:]
let g be Function of V,Z; :: thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:]

per cases not ( [:Y,Z:] = {} & not [:X,V:] = {} & not ( [:Y,Z:] = {} & [:X,V:] <> {} ) ) ;

suppose A1: ( [:Y,Z:] = {} implies [:X,V:] = {} ) ; :: thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:]

now

per cases ( [:Y,Z:] <> {} or [:X,V:] = {} ) by A1;

suppose [:Y,Z:] <> {} ; :: thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:]

then A2: ( ( Y = {} implies X = {} ) & ( Z = {} implies V = {} ) ) by ZFMISC_1:113;
( rng f c= Y & rng g c= Z ) by RELAT_1:def 19;
then ( [:(rng f),(rng g):] c= [:Y,Z:] & rng [:f,g:] = [:(rng f),(rng g):] ) by Th88, ZFMISC_1:119;
then ( dom f = X & dom g = V & rng [:f,g:] c= [:Y,Z:] ) by A2, FUNCT_2:def 1;
then ( dom [:f,g:] = [:X,V:] & rng [:f,g:] c= [:Y,Z:] ) by Def9;
hence [:f,g:] is Function of [:X,V:],[:Y,Z:] by A1, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

suppose A3: [:X,V:] = {} ; :: thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:]

then ( X = {} or V = {} ) ;
then ( dom f = {} or dom g = {} ) ;
then [:(dom f),(dom g):] = {} by ZFMISC_1:113;
then A4: dom [:f,g:] = [:X,V:] by A3, Def9;
( rng f c= Y & rng g c= Z ) by RELAT_1:def 19;
then [:(rng f),(rng g):] c= [:Y,Z:] by ZFMISC_1:119;
then rng [:f,g:] c= [:Y,Z:] by Th88;
hence [:f,g:] is Function of [:X,V:],[:Y,Z:] by A1, A4, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

end;

end;

hence [:f,g:] is Function of [:X,V:],[:Y,Z:] ; :: thesis: verum

end;

suppose A5: ( [:Y,Z:] = {} & [:X,V:] <> {} ) ; :: thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:]

then ( ( Y = {} or Z = {} ) & X <> {} & V <> {} ) by ZFMISC_1:113;
then ( f = {} or g = {} ) ;
then [:(dom f),(dom g):] = {} by RELAT_1:60, ZFMISC_1:113;
then A6: dom [:f,g:] = {} by Def9;
then A7: [:f,g:] = {} ;
rng [:f,g:] = {} by A6, RELAT_1:65;
then ( dom [:f,g:] c= [:X,V:] & rng [:f,g:] c= [:Y,Z:] ) by A6, XBOOLE_1:2;
then reconsider R = [:f,g:] as Relation of [:X,V:],[:Y,Z:] by RELSET_1:11;
R is quasi_total by A5, A7, FUNCT_2:def 1;
hence [:f,g:] is Function of [:X,V:],[:Y,Z:] ; :: thesis: verum

end;

end;