set H = f1 +* f2;
set G = f2 +* f1;
A2: ( dom f1 = A1 & dom f2 = A2 ) by FUNCT_2:def 1;
then A3: ( dom (f1 +* f2) = A1 \/ A2 & dom (f2 +* f1) = A1 \/ A2 ) by FUNCT_4:def 1;
reconsider A0 = A1 \/ A2 as non empty Subset of A ;

A4: now

let a be Element of A0; :: thesis: ( ( a in A1 implies (f2 +* f1) . a = f1 . a ) & ( a in A2 \ A1 implies (f2 +* f1) . a = f2 . a ) )
thus ( a in A1 implies (f2 +* f1) . a = f1 . a ) by A2, FUNCT_4:def 1; :: thesis: ( a in A2 \ A1 implies (f2 +* f1) . a = f2 . a )
thus ( a in A2 \ A1 implies (f2 +* f1) . a = f2 . a ) :: thesis: verum

proof

assume a in A2 \ A1 ; :: thesis: (f2 +* f1) . a = f2 . a
then not a in A1 by XBOOLE_0:def 5;
hence (f2 +* f1) . a = f2 . a by A2, FUNCT_4:def 1; :: thesis: verum

end;

end;

A5: now

let a be Element of A0; :: thesis: ( ( a in A2 implies (f1 +* f2) . a = f2 . a ) & ( a in A1 \ A2 implies (f1 +* f2) . a = f1 . a ) )
thus ( a in A2 implies (f1 +* f2) . a = f2 . a ) by A2, FUNCT_4:def 1; :: thesis: ( a in A1 \ A2 implies (f1 +* f2) . a = f1 . a )
thus ( a in A1 \ A2 implies (f1 +* f2) . a = f1 . a ) :: thesis: verum

proof

assume a in A1 \ A2 ; :: thesis: (f1 +* f2) . a = f1 . a
then not a in A2 by XBOOLE_0:def 5;
hence (f1 +* f2) . a = f1 . a by A2, FUNCT_4:def 1; :: thesis: verum

end;

end;

( rng (f1 +* f2) c= (rng f1) \/ (rng f2) & rng (f2 +* f1) c= (rng f2) \/ (rng f1) ) by FUNCT_4:18;
then A6: ( rng (f2 +* f1) c= B & rng (f1 +* f2) c= B ) by XBOOLE_1:1;
then reconsider F0 = f1 +* f2 as Function of (A1 \/ A2),B by A3, FUNCT_2:def 1, RELSET_1:11;
reconsider F1 = f2 +* f1 as Function of (A1 \/ A2),B by A3, A6, FUNCT_2:def 1, RELSET_1:11;

A7: now

let a be Element of A0; :: thesis: F0 . a = F1 . a

A8: now

assume A9: a in A1 \+\ A2 ; :: thesis: F0 . a = F1 . a

A10: now

assume A11: a in A1 \ A2 ; :: thesis: F0 . a = F1 . a
A12: A1 \ A2 c= A1 by XBOOLE_1:36;
thus F0 . a = f1 . a by A5, A11
.= F1 . a by A4, A11, A12 ; :: thesis: verum

end;

now

assume A13: a in A2 \ A1 ; :: thesis: F0 . a = F1 . a
A2 \ A1 c= A2 by XBOOLE_1:36;
hence F0 . a = f2 . a by A5, A13
.= F1 . a by A4, A13 ;
:: thesis: verum

end;

hence F0 . a = F1 . a by A9, A10, XBOOLE_0:def 3; :: thesis: verum

end;

A14: now

assume A15: a in A1 /\ A2 ; :: thesis: F0 . a = F1 . a
then A16: ( a in A1 & a in A2 ) by XBOOLE_0:def 4;
A17: f1 . a = (f2 | (A1 /\ A2)) . a by A1, A15, FUNCT_1:72
.= f2 . a by A15, FUNCT_1:72 ;
( F0 . a = f2 . a & F1 . a = f1 . a ) by A4, A5, A16;
hence F0 . a = F1 . a by A17; :: thesis: verum

end;

( A0 = (A1 \+\ A2) \/ (A1 /\ A2) & a in A0 ) by XBOOLE_1:93;
hence F0 . a = F1 . a by A8, A14, XBOOLE_0:def 3; :: thesis: verum

end;

take F0 ; :: thesis: ( F0 | A1 = f1 & F0 | A2 = f2 )

now

thus A1 is non empty Subset of A0 by XBOOLE_1:7; :: thesis: for a being Element of A0 st a in A1 holds
F0 . a = f1 . a
let a be Element of A0; :: thesis: ( a in A1 implies F0 . a = f1 . a )
assume A18: a in A1 ; :: thesis: F0 . a = f1 . a
thus F0 . a = F1 . a by A7
.= f1 . a by A4, A18 ; :: thesis: verum

end;

hence F0 | A1 = f1 by FUNCT_2:173; :: thesis: F0 | A2 = f2
( A2 is non empty Subset of A0 & ( for a being Element of A0 st a in A2 holds
F0 . a = f2 . a ) ) by A5, XBOOLE_1:7;
hence F0 | A2 = f2 by FUNCT_2:173; :: thesis: verum