let f, g be Function; :: thesis: for x being Element of [:f,g:] st f <> {} & g <> {} holds
( x `1 is pair & x `2 is pair )
set F = [:f,g:];
set D = dom [:f,g:];
set C = rng [:f,g:];
set df = dom f;
set dg = dom g;
set rf = rng f;
set rg = rng g;
let x be Element of [:f,g:]; :: thesis: ( f <> {} & g <> {} implies ( x `1 is pair & x `2 is pair ) )
assume ( f <> {} & g <> {} ) ; :: thesis: ( x `1 is pair & x `2 is pair )
then reconsider U = [:[:(dom f),(dom g):],[:(rng f),(rng g):]:] as non empty Relation ;
A1: ( [:f,g:] c= [:(dom [:f,g:]),(rng [:f,g:]):] & dom [:f,g:] = [:(dom f),(dom g):] & rng [:f,g:] = [:(rng f),(rng g):] ) by FUNCT_3:def 8, RELAT_1:7, FUNCT_3:67;
then reconsider F = [:f,g:] as Relation-like Function-like Subset of U ;
F <> {} by A1;
then x in F ;
then reconsider xx = x as Element of U ;
consider a, b being object such that
A2: ( a in [:(dom f),(dom g):] & b in [:(rng f),(rng g):] & xx = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as set by TARSKI:1;
thus ( x `1 is pair & x `2 is pair ) by A2; :: thesis: verum