let X, Y1, Y2 be set ; :: thesis: for f1 being Function of X,Y1
for f2 being Function of X,Y2 holds <:f1,f2:> = [:f1,f2:] * (delta X)
let f1 be Function of X,Y1; :: thesis: for f2 being Function of X,Y2 holds <:f1,f2:> = [:f1,f2:] * (delta X)
let f2 be Function of X,Y2; :: thesis: <:f1,f2:> = [:f1,f2:] * (delta X)

per cases ( Y1 = {} or Y2 = {} or ( Y1 <> {} & Y2 <> {} ) ) ;

suppose ( Y1 = {} or Y2 = {} ) ; :: thesis: <:f1,f2:> = [:f1,f2:] * (delta X)

then A1: ( dom f1 = {} or dom f2 = {} ) ;
A2: dom [:f1,f2:] = [:(dom f1),(dom f2):] by Def9
.= {} by A1, ZFMISC_1:113 ;
dom <:f1,f2:> = (dom f1) /\ (dom f2) by Def8
.= {} by A1 ;
hence <:f1,f2:> = {} * (delta X)
.= [:f1,f2:] * (delta X) by A2, RELAT_1:64 ;
:: thesis: verum

end;

suppose ( Y1 <> {} & Y2 <> {} ) ; :: thesis: <:f1,f2:> = [:f1,f2:] * (delta X)

then ( dom f1 = X & dom f2 = X ) by FUNCT_2:def 1;
hence <:f1,f2:> = [:f1,f2:] * (delta X) by Th89; :: thesis: verum

end;

end;