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):>;

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]end;

hence
<:(X --> x1),(X --> x2):> = X --> [x1,x2]
; :: thesis: verumper cases
( X = {} or X <> {} )
;

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;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