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 ;
then <:(X --> x1),(X --> x2):> . the Element of X = [x1,x2] by ;
then [x1,x2] in rng <:(X --> x1),(X --> x2):> by ;
then {[x1,x2]} c= rng <:(X --> x1),(X --> x2):> by ZFMISC_1:31;
then rng <:(X --> x1),(X --> x2):> = {[x1,x2]} by ;
hence <:(X --> x1),(X --> x2):> = X --> [x1,x2] by ; :: thesis: verum
end;
end;
end;
hence <:(X --> x1),(X --> x2):> = X --> [x1,x2] ; :: thesis: verum