let X1, X2 be set ; for a1, a2 being set holds [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
let a1, a2 be set ; [:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
A2:
dom ([:X1,X2:] --> [a1,a2]) = [:(dom (X1 --> a1)),(dom (X2 --> a2)):]
;
now 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 ;
( 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) )
;
([: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;
verum end;
hence
[:(X1 --> a1),(X2 --> a2):] = [:X1,X2:] --> [a1,a2]
by A2, FUNCT_3:def 8; verum