let X1, X2 be set ; :: thesis: for a1, a2 being set holds [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
let a1, a2 be set ; :: thesis: [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
A2: dom ([:X1,X2:] --> [a1,a2]) = [:(dom (X1 --> a1)),(dom (X2 --> a2)):] ;

now :: thesis: for x, y being object st x in dom (X1 --> a1) & y in dom (X2 --> a2) holds
([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)]

let x, y be object ; :: thesis: ( x in dom (X1 --> a1) & y in dom (X2 --> a2) implies ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)] )
assume A3: ( x in dom (X1 --> a1) & y in dom (X2 --> a2) ) ; :: thesis: ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)]
then [x,y] in dom ([:X1,X2:] --> [a1,a2]) by ZFMISC_1:87;
then A4: [x,y] in [:X1,X2:] ;
( (X1 --> a1) . x = a1 & (X2 --> a2) . y = a2 ) by A3, FUNCOP_1:7;
hence ([:X1,X2:] --> [a1,a2]) . (x,y) = [((X1 --> a1) . x),((X2 --> a2) . y)] by A4, FUNCOP_1:7; :: thesis: verum

end;

hence [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2] by A2, FUNCT_3:def 8; :: thesis: verum