deffunc H₁( set ) -> Element of F₁() = F₅() . F₃();
deffunc H₂( set ) -> set = F₄() . $1;
defpred S₁[ set ] means for x1 being bound_QC-variable st x1 = $1 holds
x1 <> F₂();
A1: for x being set st x in bound_QC-variables holds
( ( S₁[x] implies H₂(x) in F₁() ) & ( not S₁[x] implies H₁(x) in F₁() ) ) by FUNCT_2:7;
consider f being Function of bound_QC-variables ,F₁() such that
A2: for x being set st x in bound_QC-variables holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₁(x) ) ) from FUNCT_2:sch 5(A1);
( dom f = bound_QC-variables & rng f c= F₁() ) by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider f = f as Element of Valuations_in F₁() by FUNCT_2:def 2;
take f ; :: thesis: ( ( for x being bound_QC-variable st x <> F₂() holds
f . x = F₄() . x ) & f . F₂() = F₅() . F₃() )

now

let x be bound_QC-variable; :: thesis: ( ( x <> F₂() implies f . x = F₄() . x ) & ( x = F₂() implies f . F₂() = F₅() . F₃() ) )

now

assume A3: x <> F₂() ; :: thesis: f . x = F₄() . x
( ( for x1 being bound_QC-variable st x1 = x holds
x1 <> F₂() ) implies f . x = F₄() . x ) by A2;
hence f . x = F₄() . x by A3; :: thesis: verum

end;

hence ( x <> F₂() implies f . x = F₄() . x ) ; :: thesis: ( x = F₂() implies f . F₂() = F₅() . F₃() )
thus ( x = F₂() implies f . F₂() = F₅() . F₃() ) by A2; :: thesis: verum

end;

hence ( ( for x being bound_QC-variable st x <> F₂() holds
f . x = F₄() . x ) & f . F₂() = F₅() . F₃() ) ; :: thesis: verum