let x, X be set ; :: thesis: for f, g being Function st dom f = X & dom g = X & x in X holds
<:f,g:> . x = [(f . x),(g . x)]
let f, g be Function; :: thesis: ( dom f = X & dom g = X & x in X implies <:f,g:> . x = [(f . x),(g . x)] )
assume ( dom f = X & dom g = X & x in X ) ; :: thesis: <:f,g:> . x = [(f . x),(g . x)]
then x in (dom f) /\ (dom g) ;
then x in dom <:f,g:> by Def7;
hence <:f,g:> . x = [(f . x),(g . x)] by Def7; :: thesis: verum