thus ex F being Function of F₁(),F₂() st
for x being set st x in F₁() holds
F /. x = F₃(x) from CAT_3:sch 1(); :: thesis: for F1, F2 being Function of F₁(),F₂() st ( for x being set st x in F₁() holds
F1 /. x = F₃(x) ) & ( for x being set st x in F₁() holds
F2 /. x = F₃(x) ) holds
F1 = F2
let F1, F2 be Function of F₁(),F₂(); :: thesis: ( ( for x being set st x in F₁() holds
F1 /. x = F₃(x) ) & ( for x being set st x in F₁() holds
F2 /. x = F₃(x) ) implies F1 = F2 )
assume that
A1: for x being set st x in F₁() holds
F1 /. x = F₃(x) and
A2: for x being set st x in F₁() holds
F2 /. x = F₃(x) ; :: thesis: F1 = F2

now :: thesis: for x being set st x in F₁() holds
F1 /. x = F2 /. x

let x be set ; :: thesis: ( x in F₁() implies F1 /. x = F2 /. x )
assume A3: x in F₁() ; :: thesis: F1 /. x = F2 /. x
hence F1 /. x = F₃(x) by A1
.= F2 /. x by A2, A3 ;
:: thesis: verum

end;

hence F1 = F2 by Th1; :: thesis: verum