let a1, a2, b1, b2 be set ; :: thesis: for f, g being Function holds
( [[a1,a2],[b1,b2]] in [:f,g:] iff ( [a1,b1] in f & [a2,b2] in g ) )
let f, g be Function; :: thesis: ( [[a1,a2],[b1,b2]] in [:f,g:] iff ( [a1,b1] in f & [a2,b2] in g ) )
set a = [a1,a2];
set b = [b1,b2];
set F = [:f,g:];
thus ( [[a1,a2],[b1,b2]] in [:f,g:] implies ( [a1,b1] in f & [a2,b2] in g ) ) :: thesis: ( [a1,b1] in f & [a2,b2] in g implies [[a1,a2],[b1,b2]] in [:f,g:] )

proof

assume A1: [[a1,a2],[b1,b2]] in [:f,g:] ; :: thesis: ( [a1,b1] in f & [a2,b2] in g )
then reconsider F = [:f,g:] as non empty Function ;
set D = dom F;
set C = rng F;
F <> {} ;
then reconsider ff = f, gg = g as non empty Function ;
set df = dom ff;
set dg = dom gg;
set rf = rng ff;
set rg = rng gg;
reconsider ff = ff as Function of (dom ff),(rng ff) by FUNCT_2:1;
reconsider gg = gg as Function of (dom gg),(rng gg) by FUNCT_2:1;
A2: ( [a1,a2] in dom F & [b1,b2] = [:ff,gg:] . (a1,a2) ) by FUNCT_1:1, A1;
reconsider aa = [a1,a2] as Element of dom F by FUNCT_1:1, A1;
reconsider aaa = aa as Element of [:(dom ff),(dom gg):] by FUNCT_3:def 8;
A3: ( {(aaa `1)} \ (dom ff) = {} & {(aaa `2)} \ (dom gg) = {} & [a1,a2] `1 = a1 & [a1,a2] `2 = a2 ) ;
reconsider a1 = a1 as Element of dom ff by A3;
reconsider a2 = a2 as Element of dom gg by A3;
( [b1,b2] = [(ff . a1),(gg . a2)] & [(ff . a1),(gg . a2)] `1 = ff . a1 & [b1,b2] `1 = b1 & [(ff . a1),(gg . a2)] `2 = gg . a2 & [b1,b2] `2 = b2 ) by A2, FUNCT_3:75;
hence ( [a1,b1] in f & [a2,b2] in g ) by FUNCT_1:def 2; :: thesis: verum

end;

assume A4: ( [a1,b1] in f & [a2,b2] in g ) ; :: thesis: [[a1,a2],[b1,b2]] in [:f,g:]
then reconsider ff = f, gg = g as non empty Function ;
set df = dom f;
set dg = dom g;
( a1 in dom f & b1 = ff . a1 & a2 in dom g & b2 = gg . a2 ) by FUNCT_1:1, A4;
then [b1,b2] = [:f,g:] . (a1,a2) by FUNCT_3:def 8
.= [:f,g:] . [a1,a2] ;
then ( [:f,g:] . [a1,a2] = [b1,b2] & [a1,a2] in dom [:f,g:] ) by FUNCT_1:def 2;
hence [[a1,a2],[b1,b2]] in [:f,g:] by FUNCT_1:def 2; :: thesis: verum