let A, B be non empty set ; :: thesis:
let A1, A2 be non empty Subset of A; :: thesis:
let f1 be Function of A1,B; :: thesis:
let f2 be Function of A2,B; :: thesis:
assume A1: f1 | (A1 /\ A2) = f2 | (A1 /\ A2) ; :: thesis:
A2: ( dom f1 = A1 & dom f2 = A2 ) by FUNCT_2:def 1;
for x being object st x in (dom f1) /\ (dom f2) holds
f1 . x = f2 . x

let x be object ; :: thesis:
assume a3: x in (dom f1) /\ (dom f2) ; :: thesis:
then f1 . x = (f1 | (A1 /\ A2)) . x by A2, FUNCT_1:49
.= f2 . x by FUNCT_1:49, a3, A2, A1 ;
hence f1 . x = f2 . x ; :: thesis:

end;