reconsider A0 = A1 \/ A2 as non empty Subset of A ;
set G = f2 +* f1;
set H = f1 +* f2;
rng (f1 +* f2) c= (rng f1) \/ (rng f2) by FUNCT_4:17;
then A2: rng (f1 +* f2) c= B by XBOOLE_1:1;
rng (f2 +* f1) c= (rng f2) \/ (rng f1) by FUNCT_4:17;
then A3: rng (f2 +* f1) c= B by XBOOLE_1:1;
A4: ( dom f1 = A1 & dom f2 = A2 ) by FUNCT_2:def 1;
then dom (f1 +* f2) = A1 \/ A2 by FUNCT_4:def 1;
then reconsider F0 = f1 +* f2 as Function of (A1 \/ A2),B by A2, FUNCT_2:def 1, RELSET_1:4;
dom (f2 +* f1) = A1 \/ A2 by A4, FUNCT_4:def 1;
then reconsider F1 = f2 +* f1 as Function of (A1 \/ A2),B by A3, FUNCT_2:def 1, RELSET_1:4;
take F0 ; :: thesis: ( F0 | A1 = f1 & F0 | A2 = f2 )

A5: now :: thesis: for a being Element of A0 holds
( ( a in A2 implies (f1 +* f2) . a = f2 . a ) & ( a in A1 \ A2 implies (f1 +* f2) . a = f1 . a ) )

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 A4, 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 A4, FUNCT_4:def 1; :: thesis: verum

end;

end;

A6: now :: thesis: for a being Element of A0 holds
( ( a in A1 implies (f2 +* f1) . a = f1 . a ) & ( a in A2 \ A1 implies (f2 +* f1) . a = f2 . a ) )

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 A4, 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 A4, FUNCT_4:def 1; :: thesis: verum

end;

end;

A7: now :: thesis: for a being Element of A0 holds F0 . a = F1 . a

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

A8: now :: thesis: ( a in A1 /\ A2 implies F0 . a = F1 . a )

assume A9: a in A1 /\ A2 ; :: thesis: F0 . a = F1 . a
then A10: a in A1 by XBOOLE_0:def 4;
a in A2 by A9, XBOOLE_0:def 4;
then A11: F0 . a = f2 . a by A5;
f1 . a = (f2 | (A1 /\ A2)) . a by A1, A9, FUNCT_1:49
.= f2 . a by A9, FUNCT_1:49 ;
hence F0 . a = F1 . a by A6, A10, A11; :: thesis: verum

end;

A12: now :: thesis: ( a in A1 \+\ A2 implies F0 . a = F1 . a )

A13: now :: thesis: ( a in A2 \ A1 implies F0 . a = F1 . a )

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

end;

A15: now :: thesis: ( a in A1 \ A2 implies F0 . a = F1 . a )

A16: A1 \ A2 c= A1 by XBOOLE_1:36;
assume A17: a in A1 \ A2 ; :: thesis: F0 . a = F1 . a
hence F0 . a = f1 . a by A5
.= F1 . a by A6, A17, A16 ;
:: thesis: verum

end;

assume a in A1 \+\ A2 ; :: thesis: F0 . a = F1 . a
hence F0 . a = F1 . a by A15, A13, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

now :: thesis: ( A1 is non empty Subset of A0 & ( for a being Element of A0 st a in A1 holds
F0 . a = f1 . a ) )

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 A6, A18 ; :: thesis: verum

end;

hence F0 | A1 = f1 by FUNCT_2:96; :: thesis: F0 | A2 = f2
A2 is non empty Subset of A0 by XBOOLE_1:7;
hence F0 | A2 = f2 by A5, FUNCT_2:96; :: thesis: verum