reconsider A0 = A1 \/ A2 as non empty Subset of A ;
let F, G be Function of (A1 \/ A2),B; :: thesis: ( F | A1 = f1 & F | A2 = f2 & G | A1 = f1 & G | A2 = f2 implies F = G )
assume that
A19: F | A1 = f1 and
A20: F | A2 = f2 and
A21: G | A1 = f1 and
A22: G | A2 = f2 ; :: thesis: F = G

now

let a be Element of A0; :: thesis: F . a = G . a

A23: now

assume A24: a in A2 ; :: thesis: F . a = G . a
hence F . a = (G | A2) . a by A20, A22, FUNCT_1:72
.= G . a by A24, FUNCT_1:72 ;
:: thesis: verum

end;

now

assume A25: a in A1 ; :: thesis: F . a = G . a
hence F . a = (G | A1) . a by A19, A21, FUNCT_1:72
.= G . a by A25, FUNCT_1:72 ;
:: thesis: verum

end;

hence F . a = G . a by A23, XBOOLE_0:def 3; :: thesis: verum

end;

hence F = G by FUNCT_2:113; :: thesis: verum