let b1, b2 be set ; :: thesis: for f1, f2 being Function st (rng f1) /\ (rng f2) = {} & b1 <> b2 & rng f1 c= dom f2 & rng f2 c= dom f1 holds
[:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1))
let f1, f2 be Function; :: thesis: ( (rng f1) /\ (rng f2) = {} & b1 <> b2 & rng f1 c= dom f2 & rng f2 c= dom f1 implies [:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1)) )
set A1 = dom f1;
set A2 = dom f2;
set g1 = [:(rng f1),{b2}:];
set g2 = [:(rng f2),{b1}:];
set h1 = b1 .--> b2;
set h2 = b2 .--> b1;
set h = (b1,b2) --> (b2,b1);
set f = f1 \/ f2;
set g = [:(rng f1),{b2}:] \/ [:(rng f2),{b1}:];
assume (rng f1) /\ (rng f2) = {} ; :: thesis: ( not b1 <> b2 or not rng f1 c= dom f2 or not rng f2 c= dom f1 or [:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1)) )
then reconsider e = (rng f1) /\ (rng f2) as empty set ;
A1: (dom [:(rng f1),{b2}:]) /\ (rng f2) = (dom [:(rng f1),{b2}:]) /\ e
.= {} ;
A2: (dom [:(rng f2),{b1}:]) /\ (rng f1) = (dom [:(rng f2),{b1}:]) /\ e
.= {} ;
A3: (((rng [:(dom f1),{b2}:]) /\ {b2}) /\ {b1}) \+\ ((rng [:(dom f1),{b2}:]) /\ ({b2} /\ {b1})) = {} ;
((rng [:(dom f1),{b2}:]) /\ {b2}) \+\ (rng [:(dom f1),{b2}:]) = {} ;
then A4: (rng [:(dom f1),{b2}:]) /\ {b1} = ((rng [:(dom f1),{b2}:]) /\ {b2}) /\ {b1} by Th29
.= (rng [:(dom f1),{b2}:]) /\ ({b1} /\ {b2}) by A3, Th29 ;
(f1 \/ f2) * ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:]) = ((f1 \/ f2) >*> [:(rng f1),{b2}:]) \/ ((f1 \/ f2) >*> [:(rng f2),{b1}:]) by RELAT_1:32
.= ((f1 >*> [:(rng f1),{b2}:]) \/ (f2 >*> [:(rng f1),{b2}:])) \/ ((f1 \/ f2) >*> [:(rng f2),{b1}:]) by SYSREL:6
.= ((f1 >*> [:(rng f1),{b2}:]) \/ (f2 >*> [:(rng f1),{b2}:])) \/ ((f1 >*> [:(rng f2),{b1}:]) \/ (f2 >*> [:(rng f2),{b1}:])) by SYSREL:6
.= ((f1 >*> [:(rng f1),{b2}:]) \/ (f2 >*> [:(rng f1),{b2}:])) \/ ({} \/ (f2 >*> [:(rng f2),{b1}:])) by A2, XBOOLE_0:def 7, RELAT_1:44
.= (((f1 >*> [:(rng f1),{b2}:]) \/ {}) \/ {}) \/ (f2 >*> [:(rng f2),{b1}:]) by A1, XBOOLE_0:def 7, RELAT_1:44
.= [:(dom f1),{b2}:] \/ (f2 >*> [:(rng f2),{b1}:]) by Lm63
.= [:(dom f1),{b2}:] \/ [:(dom f2),{b1}:] by Lm63 ;
then A5: ((f1 \/ f2) * ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1 .--> b2) \/ (b2 .--> b1)) = ([:(dom f1),{b2}:] >*> ((b1 .--> b2) \/ (b2 .--> b1))) \/ ([:(dom f2),{b1}:] >*> ((b1 .--> b2) \/ (b2 .--> b1))) by SYSREL:6
.= (([:(dom f1),{b2}:] >*> (b1 .--> b2)) \/ ([:(dom f1),{b2}:] >*> (b2 .--> b1))) \/ ([:(dom f2),{b1}:] >*> ((b1 .--> b2) \/ (b2 .--> b1))) by RELAT_1:32
.= (([:(dom f1),{b2}:] >*> (b1 .--> b2)) \/ ([:(dom f1),{b2}:] >*> (b2 .--> b1))) \/ (([:(dom f2),{b1}:] >*> (b1 .--> b2)) \/ ([:(dom f2),{b1}:] >*> (b2 .--> b1))) by RELAT_1:32 ;
assume A6: b1 <> b2 ; :: thesis: ( not rng f1 c= dom f2 or not rng f2 c= dom f1 or [:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1)) )
then A7: {b1} /\ {b2} = {} by XBOOLE_0:def 7, ZFMISC_1:11;
then {} = (rng [:(dom f1),{b2}:]) /\ (dom (b1 .--> b2)) by A4;
then A8: ((f1 \/ f2) * ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1 .--> b2) \/ (b2 .--> b1)) = ({} \/ ([:(dom f1),{b2}:] >*> (b2 .--> b1))) \/ (([:(dom f2),{b1}:] >*> (b1 .--> b2)) \/ ([:(dom f2),{b1}:] >*> (b2 .--> b1))) by RELAT_1:44, A5, XBOOLE_0:def 7;
A9: ((rng [:(dom f2),{b1}:]) /\ ({b1} /\ {b2})) \+\ (((rng [:(dom f2),{b1}:]) /\ {b1}) /\ {b2}) = {} ;
((rng [:(dom f2),{b1}:]) /\ {b1}) \+\ (rng [:(dom f2),{b1}:]) = {} ;
then (rng [:(dom f2),{b1}:]) /\ {b2} = ((rng [:(dom f2),{b1}:]) /\ {b1}) /\ {b2} by Th29
.= (rng [:(dom f2),{b1}:]) /\ ({b1} /\ {b2}) by A9, Th29 ;
then (rng [:(dom f2),{b1}:]) /\ (dom (b2 .--> b1)) = {} by A7;
then [:(dom f2),{b1}:] >*> (b2 .--> b1) = {} by RELAT_1:44, XBOOLE_0:def 7;
then A10: ((f1 \/ f2) * ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1 .--> b2) \/ (b2 .--> b1)) = ([:(dom f1),{b2}:] >*> (b2 .--> b1)) \/ [:(((dom f2) --> b1) " {b1}),{b2}:] by Lm61, A8
.= ([:(dom f1),{b2}:] >*> (b2 .--> b1)) \/ [:(dom f2),{b2}:] by FUNCOP_1:15
.= [:(((dom f1) --> b2) " {b2}),{b1}:] \/ [:(dom f2),{b2}:] by Lm61
.= [:(dom f1),{b1}:] \/ ((dom f2) --> b2) by FUNCOP_1:15 ;
assume rng f1 c= dom f2 ; :: thesis: ( not rng f2 c= dom f1 or [:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1)) )
then reconsider B1 = rng f1 as Subset of (dom f2) ;
assume rng f2 c= dom f1 ; :: thesis: [:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1))
then reconsider B2 = rng f2 as Subset of (dom f1) ;
( [:B1,{b2}:] \ [:((dom f2) null B1),({b2} \/ {}):] = {} & [:B2,{b1}:] \ [:((dom f1) null B2),({b1} \/ {}):] = {} ) ;
then A11: ( B1 --> b2 c= (dom f2) --> b2 & B2 --> b1 c= (dom f1) --> b1 ) by Th29;
(b1,b2) --> (b2,b1) = [:({b1} \ {b2}),{b2}:] \/ (b2 .--> b1) by ZFMISC_1:102
.= (b1 .--> b2) \/ (b2 .--> b1) by A6, ZFMISC_1:11, XBOOLE_1:83 ;
hence [:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1)) by A11, A10, XBOOLE_1:13; :: thesis: verum