A1:
dom <:x,y:> = (dom x) /\ (dom y)
by FUNCT_3:def 7;
rng <:x,y:> c= [:(rng x),(rng y):]
by FUNCT_3:51;
then
rng <:x,y:> c= [:REAL,REAL:]
by XBOOLE_1:1;
then reconsider xy = <:x,y:> as PartFunc of REAL,[:REAL,REAL:] by A1, RELSET_1:4;
((Re f) * R2-to-C) * xy is PartFunc of REAL,REAL
;
then reconsider u0 = ((Re f) * R2-to-C) * <:x,y:> as PartFunc of REAL,REAL ;
((Im f) * R2-to-C) * xy is PartFunc of REAL,REAL
;
then reconsider v0 = ((Im f) * R2-to-C) * <:x,y:> as PartFunc of REAL,REAL ;
(integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) is Complex
;
hence
ex b1 being Complex ex u0, v0 being PartFunc of REAL,REAL st
( u0 = ((Re f) * R2-to-C) * <:x,y:> & v0 = ((Im f) * R2-to-C) * <:x,y:> & b1 = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) )
; verum