let X be set ; :: thesis: for f, g being Function st dom f = X & dom g = X holds
<:f,g:> = [:f,g:] * (delta X)
let f, g be Function; :: thesis: ( dom f = X & dom g = X implies <:f,g:> = [:f,g:] * (delta X) )
assume A1: ( dom f = X & dom g = X ) ; :: thesis: <:f,g:> = [:f,g:] * (delta X)
A2: dom (delta X) = X by Def6;
rng (delta X) c= [:X,X:] by Th47;
then rng (delta X) c= dom [:f,g:] by A1, Def8;
then A3: dom ([:f,g:] * (delta X)) = X by A2, RELAT_1:27;
(dom f) /\ (dom g) = X by A1;
then A4: dom <:f,g:> = X by Def7;
for x being object st x in X holds
<:f,g:> . x = ([:f,g:] * (delta X)) . x

proof

let x be object ; :: thesis: ( x in X implies <:f,g:> . x = ([:f,g:] * (delta X)) . x )
assume A5: x in X ; :: thesis: <:f,g:> . x = ([:f,g:] * (delta X)) . x
hence <:f,g:> . x = [(f . x),(g . x)] by A4, Def7
.= [:f,g:] . (x,x) by A1, A5, Def8
.= [:f,g:] . ((delta X) . x) by A5, Def6
.= ([:f,g:] * (delta X)) . x by A3, A5, FUNCT_1:12 ;
:: thesis: verum

end;

hence <:f,g:> = [:f,g:] * (delta X) by A4, A3; :: thesis: verum