let X be set ; for x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2]
let x1, x2 be set ; <:(X --> x1),(X --> x2):> = X --> [x1,x2]
set f = X --> x1;
set g = X --> x2;
set fg = <:(X --> x1),(X --> x2):>;
now <:(X --> x1),(X --> x2):> = X --> [x1,x2]per cases
( X = {} or X <> {} )
;
suppose A2:
X <> {}
;
<:(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;
verum end;
hence
<:(X --> x1),(X --> x2):> = X --> [x1,x2]
; verum