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 A2: [:Y,Z:] <> {} ; :: thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:]

( 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 A3: rng [:f,g:] c= [:Y,Z:] by Th88;
( Z = {} implies V = {} ) by A2, ZFMISC_1:113;
then A4: dom g = V by FUNCT_2:def 1;
( Y = {} implies X = {} ) by A2, ZFMISC_1:113;
then dom f = X by FUNCT_2:def 1;
then dom [:f,g:] = [:X,V:] by A4, Def9;
hence [:f,g:] is Function of [:X,V:],[:Y,Z:] by A1, A3, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum

end;

suppose A5: [: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 A6: dom [:f,g:] = [:X,V:] by A5, 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, A6, 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 A7: ( [:Y,Z:] = {} & [:X,V:] <> {} ) ; :: thesis: [:f,g:] is Function of [:X,V:],[:Y,Z:]

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

end;

end;