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

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:96;
then A3: rng [:f,g:] c= [:Y,Z:] by Th67;
( Z = {} implies V = {} ) by A2, ZFMISC_1:90;
then A4: dom g = V by FUNCT_2:def 1;
( Y = {} implies X = {} ) by A2, ZFMISC_1:90;
then dom f = X by FUNCT_2:def 1;
then dom [:f,g:] = [:X,V:] by A4, Def8;
hence [:f,g:] is Function of [:X,V:],[:Y,Z:] by A3, FUNCT_2:2; :: 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:90;
then A6: dom [:f,g:] = [:X,V:] by A5, Def8;
( rng f c= Y & rng g c= Z ) by RELAT_1:def 19;
then [:(rng f),(rng g):] c= [:Y,Z:] by ZFMISC_1:96;
then rng [:f,g:] c= [:Y,Z:] by Th67;
hence [:f,g:] is Function of [:X,V:],[:Y,Z:] by A6, FUNCT_2:2; :: 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 ZFMISC_1:90;
then A8: dom [:f,g:] = {} by Def8;
then ( rng [:f,g:] = {} & dom [:f,g:] c= [:X,V:] ) by RELAT_1:42;
then reconsider R = [:f,g:] as Relation of [:X,V:],[:Y,Z:] by RELSET_1:4, 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;