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 b₁ 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:> & b₁ = (integral (((u0 (#) (x `| Z)) - (v0 (#) (y `| Z))),a,b)) + ((integral (((v0 (#) (x `| Z)) + (u0 (#) (y `| Z))),a,b)) * <i>) ) ; :: thesis: verum