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 :: thesis: for a being Element of A0 holds F . a = G . a

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

A23: now :: thesis: ( a in A2 implies F . a = G . a )

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

end;

now :: thesis: ( a in A1 implies F . a = G . a )

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

end;

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

end;

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