reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def 2;
deffunc H₁( Complex, Complex) -> set = ((x1 * $1) + (x2 * $2)) + x3;
deffunc H₂( Complex, Complex) -> set = ((y1 * $1) + (y2 * $2)) + y3;
defpred S₁[ object , Element of [:COMPLEX,COMPLEX:], Element of [:COMPLEX,COMPLEX:]] means $3 = [H₁($2 `1 ,$2 `2 ),H₂($2 `1 ,$2 `2 )];
A1: for n being Nat
for x being Element of [:COMPLEX,COMPLEX:] ex y being Element of [:COMPLEX,COMPLEX:] st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of [:COMPLEX,COMPLEX:] ex y being Element of [:COMPLEX,COMPLEX:] st S₁[n,x,y]
let x be Element of [:COMPLEX,COMPLEX:]; :: thesis: ex y being Element of [:COMPLEX,COMPLEX:] st S₁[n,x,y]
reconsider a1 = H₁(x `1 ,x `2 ), a2 = H₂(x `1 ,x `2 ) as Element of COMPLEX by XCMPLX_0:def 2;
take [a1,a2] ; :: thesis: S₁[n,x,[a1,a2]]
thus S₁[n,x,[a1,a2]] ; :: thesis: verum

end;

consider f being sequence of [:COMPLEX,COMPLEX:] such that
A2: ( f . 0 = [a,b] & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
take f ; :: thesis: ( f . 0 = [a,b] & ( for n being Nat holds f . (n + 1) = [(((x1 * ((f . n) `1)) + (x2 * ((f . n) `2))) + x3),(((y1 * ((f . n) `1)) + (y2 * ((f . n) `2))) + y3)] ) )
thus ( f . 0 = [a,b] & ( for n being Nat holds f . (n + 1) = [(((x1 * ((f . n) `1)) + (x2 * ((f . n) `2))) + x3),(((y1 * ((f . n) `1)) + (y2 * ((f . n) `2))) + y3)] ) ) by A2; :: thesis: verum