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 ;
hence <:(X --> x1),(X --> x2):> = X --> [x1,x2] by A1, Th1; :: thesis: verum

end;

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

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

end;

end;

end;

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