let X be set ; :: thesis: for D1, D2 being non empty set
for f1, f2 being Function of X,D1
for g1, g2 being Function of X,D2 st <:f1,g1:> = <:f2,g2:> holds
( f1 = f2 & g1 = g2 )
let D1, D2 be non empty set ; :: thesis: for f1, f2 being Function of X,D1
for g1, g2 being Function of X,D2 st <:f1,g1:> = <:f2,g2:> holds
( f1 = f2 & g1 = g2 )
let f1, f2 be Function of X,D1; :: thesis: for g1, g2 being Function of X,D2 st <:f1,g1:> = <:f2,g2:> holds
( f1 = f2 & g1 = g2 )
let g1, g2 be Function of X,D2; :: thesis: ( <:f1,g1:> = <:f2,g2:> implies ( f1 = f2 & g1 = g2 ) )
A1: ( dom g1 = X & dom g2 = X ) by FUNCT_2:def 1;
( dom f1 = X & dom f2 = X ) by FUNCT_2:def 1;
hence ( <:f1,g1:> = <:f2,g2:> implies ( f1 = f2 & g1 = g2 ) ) by A1, Th54; :: thesis: verum