let X be set ; :: thesis: for x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2]
let x1, x2 be set ; :: thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2]
set f = X --> x1;
set g = X --> x2;
set fg = <:(X --> x1),(X --> x2):>;

now

per cases ( X = {} or X <> {} ) ;

suppose A1: X = {} ; :: thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2]

then X --> x1 = {} --> x1 ;
then <:(X --> x1),(X --> x2):> = {} --> [x1,x2] by Th1;
hence <:(X --> x1),(X --> x2):> = X --> [x1,x2] by A1; :: thesis: verum

end;

suppose A2: X <> {} ; :: thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2]

consider x being Element of X;
A3: ( dom (X --> x1) = X & dom (X --> x2) = X ) by FUNCOP_1:19;
then A4: dom <:(X --> x1),(X --> x2):> = X by FUNCT_3:70;
( (X --> x1) . x = x1 & (X --> x2) . x = x2 ) by A2, FUNCOP_1:13;
then ( <:(X --> x1),(X --> x2):> . x = [x1,x2] & rng (X --> x1) = {x1} & rng (X --> x2) = {x2} ) by A2, A3, FUNCOP_1:14, FUNCT_3:69;
then ( [x1,x2] in rng <:(X --> x1),(X --> x2):> & rng <:(X --> x1),(X --> x2):> c= [:{x1},{x2}:] ) by A2, A4, FUNCT_1:def 5, FUNCT_3:71;
then ( rng <:(X --> x1),(X --> x2):> c= {[x1,x2]} & {[x1,x2]} c= rng <:(X --> x1),(X --> x2):> ) by ZFMISC_1:35, ZFMISC_1:37;
then rng <:(X --> x1),(X --> x2):> = {[x1,x2]} by XBOOLE_0:def 10;
hence <:(X --> x1),(X --> x2):> = X --> [x1,x2] by A4, FUNCOP_1:15; :: thesis: verum

end;

end;

end;

hence <:(X --> x1),(X --> x2):> = X --> [x1,x2] ; :: thesis: verum