A1: dom <:x,y:> = (dom x) /\ (dom y) by FUNCT_3:def 8;
rng <:x,y:> c= [:(rng x),(rng y):] by FUNCT_3:71;
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:11;
((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 by XCMPLX_0:def 2;
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