let D, A, B be non empty set ; :: thesis: for H being Function of D,[:A,B:]
for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)]
let H be Function of D,[:A,B:]; :: thesis: for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)]
let d be Element of D; :: thesis: H . d = [((pr1 H) . d),((pr2 H) . d)]
thus H . d = [((H . d) `1 ),((H . d) `2 )] by MCART_1:23
.= [((H . d) `1 ),((pr2 H) . d)] by Def7
.= [((pr1 H) . d),((pr2 H) . d)] by Def6 ; :: thesis: verum