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