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 that
A1: dom f = X and
A2: dom g = X ; :: thesis: <:f,g:> = [:f,g:] * (delta X)
rng (delta X) c= [:X,X:] by Th66;
then ( rng (delta X) c= dom [:f,g:] & dom (delta X) = X & (dom f) /\ (dom g) = X ) by A1, A2, Def7, Def9;
then A3: ( dom <:f,g:> = X & dom ([:f,g:] * (delta X)) = X ) by Def8, RELAT_1:46;
for x being set st x in X holds
<:f,g:> . x = ([:f,g:] * (delta X)) . x

proof

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

end;

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