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 :: thesis: <:(X --> x1),(X --> x2):> = X --> [x1,x2]

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

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

thus <:(X --> x1),(X --> x2):> = X --> [x1,x2] by A1; :: 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:29;
set x = the Element of X;
A4: ( dom (X --> x1) = X & dom (X --> x2) = X ) ;
then A5: dom <:(X --> x1),(X --> x2):> = X by FUNCT_3:50;
( (X --> x1) . the Element of X = x1 & (X --> x2) . the Element of X = x2 ) by A2, FUNCOP_1:7;
then <:(X --> x1),(X --> x2):> . the Element of X = [x1,x2] by A2, A4, FUNCT_3:49;
then [x1,x2] in rng <:(X --> x1),(X --> x2):> by A2, A5, FUNCT_1:def 3;
then {[x1,x2]} c= rng <:(X --> x1),(X --> x2):> by ZFMISC_1:31;
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:9; :: thesis: verum

end;

end;

end;

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