deffunc H₁( object ) -> Element of NAT = F₁();
defpred S₁[ object ] means $1 = 0 ;
A3: for x being object st x in NAT holds
( ( S₁[x] implies H₁(x) in F₂() ) & ( not S₁[x] implies F₃(x) in F₂() ) ) by A1, A2;
ex f being sequence of F₂() st
for x being object st x in NAT holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = F₃(x) ) ) from FUNCT_2:sch 5(A3);
then consider f being sequence of F₂() such that
A4: for x being object st x in NAT holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = F₃(x) ) ) ;
take f ; :: thesis: ( f . 0 = F₁() & ( for x being non zero Element of NAT holds f . x = F₃(x) ) )
thus f . 0 = F₁() by A4; :: thesis: for x being non zero Element of NAT holds f . x = F₃(x)
let x be non zero Element of NAT ; :: thesis: f . x = F₃(x)
thus f . x = F₃(x) by A4; :: thesis: verum