:: CFUNCT_1 semantic presentation

begin


definition
mode Complex is complex number ;
end;

definition
let C be non empty set ;
let f1, f2 be PartFunc of C,COMPLEX;
deffunc H1( set ) ->  Element of COMPLEX = (f1 /. $1) * ((f2 /. $1) ");
funcf1 / f2 ->  PartFunc of C,COMPLEX means :Def1: :: CFUNCT_1:def 1
( dom it = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom it holds
it /. c = (f1 /. c) * ((f2 /. c) ") ) );
existence
 ex b1 being PartFunc of C,COMPLEX st
( dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 /. c) * ((f2 /. c) ") ) )
proof
defpred S1[ set ] means $1 in (dom f1) /\ ((dom f2) \ (f2 " {0c}));
consider F being PartFunc of C,COMPLEX such that
A1: for c being Element of C holds
( c in dom F iff S1[c] ) and
A2: for c being Element of C st c in dom F holds
F /. c = H1(c) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom F holds
F /. c = (f1 /. c) * ((f2 /. c) ") ) )
thus  dom F = (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, SUBSET_1:3; ::_thesis: for c being Element of C st c in dom F holds
F /. c = (f1 /. c) * ((f2 /. c) ")
thus  for c being Element of C st c in dom F holds
F /. c = (f1 /. c) * ((f2 /. c) ") by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of C,COMPLEX st dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f1 /. c) * ((f2 /. c) ") ) & dom b2 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b2 holds
b2 /. c = (f1 /. c) * ((f2 /. c) ") ) holds
b1 = b2
proof
set X = (dom f1) /\ ((dom f2) \ (f2 " {0}));
thus  for f, g being PartFunc of C,COMPLEX st dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom f holds
f /. c = H1(c) ) & dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom g holds
g /. c = H1(c) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def1 defines / CFUNCT_1:def_1_:_
 for C being non empty set
for f1, f2, b4 being PartFunc of C,COMPLEX holds
( b4 = f1 / f2 iff ( dom b4 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b4 holds
b4 /. c = (f1 /. c) * ((f2 /. c) ") ) ) );

definition
let C be non empty set ;
let f be PartFunc of C,COMPLEX;
deffunc H1( set ) ->  Element of COMPLEX = (f /. $1) " ;
funcf ^  ->  PartFunc of C,COMPLEX means :Def2: :: CFUNCT_1:def 2
( dom it = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom it holds
it /. c = (f /. c) " ) );
existence
 ex b1 being PartFunc of C,COMPLEX st
( dom b1 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f /. c) " ) )
proof
defpred S1[ set ] means $1 in (dom f) \ (f " {0c});
consider F being PartFunc of C,COMPLEX such that
A1: for c being Element of C holds
( c in dom F iff S1[c] ) and
A2: for c being Element of C st c in dom F holds
F /. c = H1(c) from PARTFUN2:sch_2();
take  F ; ::_thesis: ( dom F = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom F holds
F /. c = (f /. c) " ) )
thus  dom F = (dom f) \ (f " {0}) by A1, SUBSET_1:3; ::_thesis: for c being Element of C st c in dom F holds
F /. c = (f /. c) "
let c be Element of C; ::_thesis: ( c in dom F implies F /. c = (f /. c) " )
assume  c in dom F ; ::_thesis: F /. c = (f /. c) "
hence  F /. c = (f /. c) " by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of C,COMPLEX st dom b1 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b1 holds
b1 /. c = (f /. c) " ) & dom b2 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b2 holds
b2 /. c = (f /. c) " ) holds
b1 = b2
proof
set X = (dom f) \ (f " {0});
thus  for f, g being PartFunc of C,COMPLEX st dom f = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom f holds
f /. c = H1(c) ) & dom g = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom g holds
g /. c = H1(c) ) holds
f = g from PARTFUN2:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ^ CFUNCT_1:def_2_:_
 for C being non empty set
for f, b3 being PartFunc of C,COMPLEX holds
( b3 = f ^ iff ( dom b3 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b3 holds
b3 /. c = (f /. c) " ) ) );

theorem Th1: :: CFUNCT_1:1
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 + f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 + f2) holds
(f1 + f2) /. c = (f1 /. c) + (f2 /. c) ) )
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 + f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 + f2) holds
(f1 + f2) /. c = (f1 /. c) + (f2 /. c) ) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( dom (f1 + f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 + f2) holds
(f1 + f2) /. c = (f1 /. c) + (f2 /. c) ) )
thus A1: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1; ::_thesis: for c being Element of C st c in dom (f1 + f2) holds
(f1 + f2) /. c = (f1 /. c) + (f2 /. c)
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_f2)_holds_
(f1_+_f2)_/._c_=_(f1_/._c)_+_(f2_/._c)
let c be Element of C; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) /. c = (f1 /. c) + (f2 /. c) )
assume A2: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) /. c = (f1 /. c) + (f2 /. c)
then  c in dom f1 by A1, XBOOLE_0:def_4;
then A3: f1 . c = f1 /. c by PARTFUN1:def_6;
 c in dom f2 by A1, A2, XBOOLE_0:def_4;
then A4: f2 . c = f2 /. c by PARTFUN1:def_6;
thus (f1 + f2) /. c = (f1 + f2) . c by A2, PARTFUN1:def_6
.= (f1 /. c) + (f2 /. c) by A2, A3, A4, VALUED_1:def_1 ; ::_thesis: verum
end;
hence  for c being Element of C st c in dom (f1 + f2) holds
(f1 + f2) /. c = (f1 /. c) + (f2 /. c) ; ::_thesis: verum
end;

theorem Th2: :: CFUNCT_1:2
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) )
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) )
A1: dom (f1 - f2) = (dom f1) /\ (dom (- f2)) by VALUED_1:def_1;
hence  dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:8; ::_thesis: for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c)
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_/._c_=_(f1_/._c)_-_(f2_/._c)
let c be Element of C; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) /. c = (f1 /. c) - (f2 /. c) )
assume A2: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) /. c = (f1 /. c) - (f2 /. c)
then A3: ( dom (- f2) = dom f2 & c in dom (- f2) ) by A1, VALUED_1:8, XBOOLE_0:def_4;
 c in dom f1 by A1, A2, XBOOLE_0:def_4;
then A4: f1 /. c = f1 . c by PARTFUN1:def_6;
thus (f1 - f2) /. c = (f1 - f2) . c by A2, PARTFUN1:def_6
.= (f1 . c) - (f2 . c) by A2, VALUED_1:13
.= (f1 /. c) - (f2 /. c) by A3, A4, PARTFUN1:def_6 ; ::_thesis: verum
end;
hence  for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c) ; ::_thesis: verum
end;

theorem Th3: :: CFUNCT_1:3
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) )
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) )
thus A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4; ::_thesis: for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c)
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_(#)_f2)_holds_
(f1_(#)_f2)_/._c_=_(f1_/._c)_*_(f2_/._c)
let c be Element of C; ::_thesis: ( c in dom (f1 (#) f2) implies (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) )
assume A2: c in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c)
then  c in dom f1 by A1, XBOOLE_0:def_4;
then A3: f1 . c = f1 /. c by PARTFUN1:def_6;
 c in dom f2 by A1, A2, XBOOLE_0:def_4;
then A4: f2 . c = f2 /. c by PARTFUN1:def_6;
thus (f1 (#) f2) /. c = (f1 (#) f2) . c by A2, PARTFUN1:def_6
.= (f1 /. c) * (f2 /. c) by A2, A3, A4, VALUED_1:def_4 ; ::_thesis: verum
end;
hence  for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ; ::_thesis: verum
end;

theorem Th4: :: CFUNCT_1:4
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds
( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds
( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )
let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds
( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )
let r be Element of COMPLEX ; ::_thesis: ( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )
thus A1: dom (r (#) f) = dom f by VALUED_1:def_5; ::_thesis: for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c)
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_f)_holds_
(r_(#)_f)_/._c_=_r_*_(f_/._c)
let c be Element of C; ::_thesis: ( c in dom (r (#) f) implies (r (#) f) /. c = r * (f /. c) )
assume A2: c in dom (r (#) f) ; ::_thesis: (r (#) f) /. c = r * (f /. c)
hence (r (#) f) /. c = (r (#) f) . c by PARTFUN1:def_6
.= r * (f . c) by VALUED_1:6
.= r * (f /. c) by A1, A2, PARTFUN1:def_6 ;
::_thesis: verum
end;
hence  for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ; ::_thesis: verum
end;

theorem Th5: :: CFUNCT_1:5
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c) ) )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c) ) )
let f be PartFunc of C,COMPLEX; ::_thesis: ( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c) ) )
thus A1: dom (- f) = dom f by VALUED_1:8; ::_thesis: for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c)
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(-_f)_holds_
(-_f)_/._c_=_-_(f_/._c)
let c be Element of C; ::_thesis: ( c in dom (- f) implies (- f) /. c = - (f /. c) )
assume A2: c in dom (- f) ; ::_thesis: (- f) /. c = - (f /. c)
hence (- f) /. c = (- f) . c by PARTFUN1:def_6
.= - (f . c) by VALUED_1:8
.= - (f /. c) by A1, A2, PARTFUN1:def_6 ;
::_thesis: verum
end;
hence  for c being Element of C st c in dom (- f) holds
(- f) /. c = - (f /. c) ; ::_thesis: verum
end;

Lm1:  for x, Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( x in f " Y iff ( x in dom f & f /. x in Y ) )
by PARTFUN2:26;

theorem Th6: :: CFUNCT_1:6
for C being non empty set
for g being PartFunc of C,COMPLEX holds
( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
proof
let C be non empty set ; ::_thesis: for g being PartFunc of C,COMPLEX holds
( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
let g be PartFunc of C,COMPLEX; ::_thesis: ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
 dom (g ^) = (dom g) \ (g " {0c}) by Def2;
hence  dom (g ^) c= dom g by XBOOLE_1:36; ::_thesis: (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0})
thus  (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) by XBOOLE_1:28, XBOOLE_1:36; ::_thesis: verum
end;

theorem Th7: :: CFUNCT_1:7
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
thus  (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) c= ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) :: according to XBOOLE_0:def_10 ::_thesis: ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0})
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) or x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) )
assume A1: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) ; ::_thesis: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0}))
then A2: x in dom (f1 (#) f2) by XBOOLE_0:def_5;
reconsider x1 = x as Element of C by A1;
 not x in (f1 (#) f2) " {0c} by A1, XBOOLE_0:def_5;
then  not (f1 (#) f2) /. x1 in {0c} by A2, PARTFUN2:26;
then  (f1 (#) f2) /. x1 <> 0c by TARSKI:def_1;
then A3: (f1 /. x1) * (f2 /. x1) <> 0c by A2, Th3;
then  f2 /. x1 <> 0c ;
then  not f2 /. x1 in {0c} by TARSKI:def_1;
then A4: not x1 in f2 " {0c} by PARTFUN2:26;
A5: x1 in (dom f1) /\ (dom f2) by A2, Th3;
then  x1 in dom f2 by XBOOLE_0:def_4;
then A6: x in (dom f2) \ (f2 " {0c}) by A4, XBOOLE_0:def_5;
 f1 /. x1 <> 0c by A3;
then  not f1 /. x1 in {0c} by TARSKI:def_1;
then A7: not x1 in f1 " {0c} by PARTFUN2:26;
 x1 in dom f1 by A5, XBOOLE_0:def_4;
then  x in (dom f1) \ (f1 " {0c}) by A7, XBOOLE_0:def_5;
hence  x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) or x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) )
assume A8: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) ; ::_thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0})
then reconsider x1 = x as Element of C ;
A9: x in (dom f2) \ (f2 " {0c}) by A8, XBOOLE_0:def_4;
then A10: x in dom f2 by XBOOLE_0:def_5;
 not x in f2 " {0c} by A9, XBOOLE_0:def_5;
then  not f2 /. x1 in {0c} by A10, PARTFUN2:26;
then A11: f2 /. x1 <> 0c by TARSKI:def_1;
A12: x in (dom f1) \ (f1 " {0c}) by A8, XBOOLE_0:def_4;
then A13: x in dom f1 by XBOOLE_0:def_5;
then  x1 in (dom f1) /\ (dom f2) by A10, XBOOLE_0:def_4;
then A14: x1 in dom (f1 (#) f2) by Th3;
 not x in f1 " {0c} by A12, XBOOLE_0:def_5;
then  not f1 /. x1 in {0c} by A13, PARTFUN2:26;
then  f1 /. x1 <> 0c by TARSKI:def_1;
then  (f1 /. x1) * (f2 /. x1) <> 0c by A11, XCMPLX_1:6;
then  (f1 (#) f2) /. x1 <> 0c by A14, Th3;
then  not (f1 (#) f2) /. x1 in {0c} by TARSKI:def_1;
then  not x in (f1 (#) f2) " {0c} by PARTFUN2:26;
hence  x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by A14, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem Th8: :: CFUNCT_1:8
for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX st c in dom (f ^) holds
f /. c <> 0
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,COMPLEX st c in dom (f ^) holds
f /. c <> 0
let c be Element of C; ::_thesis: for f being PartFunc of C,COMPLEX st c in dom (f ^) holds
f /. c <> 0
let f be PartFunc of C,COMPLEX; ::_thesis: ( c in dom (f ^) implies f /. c <> 0 )
assume that
A1: c in dom (f ^) and
A2: f /. c = 0 ; ::_thesis: contradiction
A3: c in (dom f) \ (f " {0c}) by A1, Def2;
then A4: not c in f " {0c} by XBOOLE_0:def_5;
now__::_thesis:_contradiction
percases ( not c in dom f or not f /. c in {0c} ) by A4, PARTFUN2:26;
suppose not c in dom f ; ::_thesis: contradiction
hence  contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose not f /. c in {0c} ; ::_thesis: contradiction
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem Th9: :: CFUNCT_1:9
for C being non empty set
for f being PartFunc of C,COMPLEX holds (f ^) " {0} = {}
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds (f ^) " {0} = {}
let f be PartFunc of C,COMPLEX; ::_thesis: (f ^) " {0} = {}
set x = the Element of (f ^) " {0c};
assume A1: (f ^) " {0} <> {} ; ::_thesis: contradiction
then A2: the Element of (f ^) " {0c} in dom (f ^) by Lm1;
A3: (f ^) /. the Element of (f ^) " {0c} in {0c} by A1, Lm1;
reconsider x = the Element of (f ^) " {0c} as Element of C by A2;
 x in (dom f) \ (f " {0c}) by A2, Def2;
then  ( x in dom f & not x in f " {0c} ) by XBOOLE_0:def_5;
then A4: not f /. x in {0c} by PARTFUN2:26;
 (f ^) /. x = 0c by A3, TARSKI:def_1;
then  (f /. x) " = 0c by A2, Def2;
hence  contradiction by A4, TARSKI:def_1, XCMPLX_1:202; ::_thesis: verum
end;

theorem Th10: :: CFUNCT_1:10
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| " {0} = f " {0} & (- f) " {0} = f " {0} )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( |.f.| " {0} = f " {0} & (- f) " {0} = f " {0} )
let f be PartFunc of C,COMPLEX; ::_thesis: ( |.f.| " {0} = f " {0} & (- f) " {0} = f " {0} )
A1: dom |.f.| = dom f by VALUED_1:def_11;
now__::_thesis:_for_c_being_Element_of_C_holds_
(_(_c_in_|.f.|_"_{0}_implies_c_in_f_"_{0c}_)_&_(_c_in_f_"_{0c}_implies_c_in_|.f.|_"_{0}_)_)
let c be Element of C; ::_thesis: ( ( c in |.f.| " {0} implies c in f " {0c} ) & ( c in f " {0c} implies c in |.f.| " {0} ) )
thus  ( c in |.f.| " {0} implies c in f " {0c} ) ::_thesis: ( c in f " {0c} implies c in |.f.| " {0} )
proof
assume A2: c in |.f.| " {0} ; ::_thesis: c in f " {0c}
then  c in dom |.f.| by FUNCT_1:def_7;
then A3: c in dom f by VALUED_1:def_11;
 |.f.| . c in {0} by A2, FUNCT_1:def_7;
then  |.f.| . c = 0 by TARSKI:def_1;
then A4: |.(f . c).| = 0 by VALUED_1:18;
 c in dom |.f.| by A2, FUNCT_1:def_7;
then  f . c = f /. c by A1, PARTFUN1:def_6;
then  f /. c = 0c by A4, COMPLEX1:45;
then  f /. c in {0c} by TARSKI:def_1;
hence  c in f " {0c} by A3, PARTFUN2:26; ::_thesis: verum
end;
assume A5: c in f " {0c} ; ::_thesis: c in |.f.| " {0}
then  f /. c in {0c} by PARTFUN2:26;
then A6: |.(f /. c).| = 0 by COMPLEX1:44, TARSKI:def_1;
A7: c in dom f by A5, PARTFUN2:26;
then  f . c = f /. c by PARTFUN1:def_6;
then  |.f.| . c = 0 by A6, VALUED_1:18;
then A8: |.f.| . c in {0} by TARSKI:def_1;
 c in dom |.f.| by A7, VALUED_1:def_11;
hence  c in |.f.| " {0} by A8, FUNCT_1:def_7; ::_thesis: verum
end;
hence  |.f.| " {0} = f " {0} by SUBSET_1:3; ::_thesis: (- f) " {0} = f " {0}
now__::_thesis:_for_c_being_Element_of_C_holds_
(_(_c_in_(-_f)_"_{0c}_implies_c_in_f_"_{0c}_)_&_(_c_in_f_"_{0c}_implies_c_in_(-_f)_"_{0c}_)_)
let c be Element of C; ::_thesis: ( ( c in (- f) " {0c} implies c in f " {0c} ) & ( c in f " {0c} implies c in (- f) " {0c} ) )
thus  ( c in (- f) " {0c} implies c in f " {0c} ) ::_thesis: ( c in f " {0c} implies c in (- f) " {0c} )
proof
assume A9: c in (- f) " {0c} ; ::_thesis: c in f " {0c}
then A10: c in dom (- f) by PARTFUN2:26;
 (- f) /. c in {0c} by A9, PARTFUN2:26;
then  (- f) /. c = 0c by TARSKI:def_1;
then  - (- (f /. c)) = - 0c by A10, Th5;
then A11: f /. c in {0c} by TARSKI:def_1;
 c in dom f by A10, Th5;
hence  c in f " {0c} by A11, PARTFUN2:26; ::_thesis: verum
end;
assume A12: c in f " {0c} ; ::_thesis: c in (- f) " {0c}
then  f /. c in {0c} by PARTFUN2:26;
then A13: f /. c = 0c by TARSKI:def_1;
A14: c in dom f by A12, PARTFUN2:26;
then  c in dom (- f) by Th5;
then  (- f) /. c = - 0c by A13, Th5;
then A15: (- f) /. c in {0c} by TARSKI:def_1;
 c in dom (- f) by A14, Th5;
hence  c in (- f) " {0c} by A15, PARTFUN2:26; ::_thesis: verum
end;
hence  (- f) " {0} = f " {0} by SUBSET_1:3; ::_thesis: verum
end;

theorem Th11: :: CFUNCT_1:11
for C being non empty set
for f being PartFunc of C,COMPLEX holds dom ((f ^) ^) = dom (f | (dom (f ^)))
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds dom ((f ^) ^) = dom (f | (dom (f ^)))
let f be PartFunc of C,COMPLEX; ::_thesis: dom ((f ^) ^) = dom (f | (dom (f ^)))
A1: dom (f ^) = (dom f) \ (f " {0c}) by Def2;
thus  dom ((f ^) ^) = (dom (f ^)) \ ((f ^) " {0c}) by Def2
.= (dom (f ^)) \ {} by Th9
.= (dom f) /\ (dom (f ^)) by A1, XBOOLE_1:28, XBOOLE_1:36
.= dom (f | (dom (f ^))) by RELAT_1:61 ; ::_thesis: verum
end;

theorem Th12: :: CFUNCT_1:12
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st r <> 0 holds
(r (#) f) " {0} = f " {0}
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st r <> 0 holds
(r (#) f) " {0} = f " {0}
let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX st r <> 0 holds
(r (#) f) " {0} = f " {0}
let r be Element of COMPLEX ; ::_thesis: ( r <> 0 implies (r (#) f) " {0} = f " {0} )
assume A1: r <> 0 ; ::_thesis: (r (#) f) " {0} = f " {0}
now__::_thesis:_for_c_being_Element_of_C_holds_
(_(_c_in_(r_(#)_f)_"_{0c}_implies_c_in_f_"_{0c}_)_&_(_c_in_f_"_{0c}_implies_c_in_(r_(#)_f)_"_{0c}_)_)
let c be Element of C; ::_thesis: ( ( c in (r (#) f) " {0c} implies c in f " {0c} ) & ( c in f " {0c} implies c in (r (#) f) " {0c} ) )
thus  ( c in (r (#) f) " {0c} implies c in f " {0c} ) ::_thesis: ( c in f " {0c} implies c in (r (#) f) " {0c} )
proof
assume A2: c in (r (#) f) " {0c} ; ::_thesis: c in f " {0c}
then A3: c in dom (r (#) f) by PARTFUN2:26;
 (r (#) f) /. c in {0c} by A2, PARTFUN2:26;
then  (r (#) f) /. c = 0c by TARSKI:def_1;
then  r * (f /. c) = 0c by A3, Th4;
then  f /. c = 0c by A1, XCMPLX_1:6;
then A4: f /. c in {0c} by TARSKI:def_1;
 c in dom f by A3, Th4;
hence  c in f " {0c} by A4, PARTFUN2:26; ::_thesis: verum
end;
assume A5: c in f " {0c} ; ::_thesis: c in (r (#) f) " {0c}
then  f /. c in {0c} by PARTFUN2:26;
then  f /. c = 0c by TARSKI:def_1;
then A6: r * (f /. c) = 0c ;
A7: c in dom f by A5, PARTFUN2:26;
then  c in dom (r (#) f) by Th4;
then  (r (#) f) /. c = 0c by A6, Th4;
then A8: (r (#) f) /. c in {0c} by TARSKI:def_1;
 c in dom (r (#) f) by A7, Th4;
hence  c in (r (#) f) " {0c} by A8, PARTFUN2:26; ::_thesis: verum
end;
hence  (r (#) f) " {0} = f " {0} by SUBSET_1:3; ::_thesis: verum
end;

begin

theorem :: CFUNCT_1:13
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) + f3 = f1 + (f2 + f3)
proof
let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) + f3 = f1 + (f2 + f3)
let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: (f1 + f2) + f3 = f1 + (f2 + f3)
A1: dom ((f1 + f2) + f3) = (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by VALUED_1:def_1
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 + f3)) by VALUED_1:def_1
.= dom (f1 + (f2 + f3)) by VALUED_1:def_1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_+_f3)_holds_
((f1_+_f2)_+_f3)_/._c_=_(f1_+_(f2_+_f3))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) + f3) implies ((f1 + f2) + f3) /. c = (f1 + (f2 + f3)) /. c )
assume A2: c in dom ((f1 + f2) + f3) ; ::_thesis: ((f1 + f2) + f3) /. c = (f1 + (f2 + f3)) /. c
then  c in (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1;
then A3: c in dom (f1 + f2) by XBOOLE_0:def_4;
 c in (dom f1) /\ (dom (f2 + f3)) by A1, A2, VALUED_1:def_1;
then A4: c in dom (f2 + f3) by XBOOLE_0:def_4;
thus ((f1 + f2) + f3) /. c = ((f1 + f2) /. c) + (f3 /. c) by A2, Th1
.= ((f1 /. c) + (f2 /. c)) + (f3 /. c) by A3, Th1
.= (f1 /. c) + ((f2 /. c) + (f3 /. c))
.= (f1 /. c) + ((f2 + f3) /. c) by A4, Th1
.= (f1 + (f2 + f3)) /. c by A1, A2, Th1 ; ::_thesis: verum
end;
hence  (f1 + f2) + f3 = f1 + (f2 + f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th14: :: CFUNCT_1:14
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
A1: dom ((f1 (#) f2) (#) f3) = (dom (f1 (#) f2)) /\ (dom f3) by Th3
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by Th3
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 (#) f3)) by Th3
.= dom (f1 (#) (f2 (#) f3)) by Th3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_(#)_f3)_holds_
((f1_(#)_f2)_(#)_f3)_/._c_=_(f1_(#)_(f2_(#)_f3))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) (#) f3) implies ((f1 (#) f2) (#) f3) /. c = (f1 (#) (f2 (#) f3)) /. c )
assume A2: c in dom ((f1 (#) f2) (#) f3) ; ::_thesis: ((f1 (#) f2) (#) f3) /. c = (f1 (#) (f2 (#) f3)) /. c
then  c in (dom (f1 (#) f2)) /\ (dom f3) by Th3;
then A3: c in dom (f1 (#) f2) by XBOOLE_0:def_4;
 c in (dom f1) /\ (dom (f2 (#) f3)) by A1, A2, Th3;
then A4: c in dom (f2 (#) f3) by XBOOLE_0:def_4;
thus ((f1 (#) f2) (#) f3) /. c = ((f1 (#) f2) /. c) * (f3 /. c) by A2, Th3
.= ((f1 /. c) * (f2 /. c)) * (f3 /. c) by A3, Th3
.= (f1 /. c) * ((f2 /. c) * (f3 /. c))
.= (f1 /. c) * ((f2 (#) f3) /. c) by A4, Th3
.= (f1 (#) (f2 (#) f3)) /. c by A1, A2, Th3 ; ::_thesis: verum
end;
hence  (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th15: :: CFUNCT_1:15
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
proof
let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
A1: dom ((f1 + f2) (#) f3) = (dom (f1 + f2)) /\ (dom f3) by Th3
.= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by VALUED_1:def_1
.= (((dom f1) /\ (dom f2)) /\ (dom f3)) /\ (dom f3) by XBOOLE_1:16
.= (((dom f1) /\ (dom f3)) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= ((dom f1) /\ (dom f3)) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom (f1 (#) f3)) /\ ((dom f2) /\ (dom f3)) by Th3
.= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Th3
.= dom ((f1 (#) f3) + (f2 (#) f3)) by VALUED_1:def_1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_(#)_f3)_holds_
((f1_+_f2)_(#)_f3)_/._c_=_((f1_(#)_f3)_+_(f2_(#)_f3))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) (#) f3) implies ((f1 + f2) (#) f3) /. c = ((f1 (#) f3) + (f2 (#) f3)) /. c )
assume A2: c in dom ((f1 + f2) (#) f3) ; ::_thesis: ((f1 + f2) (#) f3) /. c = ((f1 (#) f3) + (f2 (#) f3)) /. c
then A3: c in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, VALUED_1:def_1;
then A4: c in dom (f1 (#) f3) by XBOOLE_0:def_4;
 c in (dom (f1 + f2)) /\ (dom f3) by A2, Th3;
then A5: c in dom (f1 + f2) by XBOOLE_0:def_4;
A6: c in dom (f2 (#) f3) by A3, XBOOLE_0:def_4;
thus ((f1 + f2) (#) f3) /. c = ((f1 + f2) /. c) * (f3 /. c) by A2, Th3
.= ((f1 /. c) + (f2 /. c)) * (f3 /. c) by A5, Th1
.= ((f1 /. c) * (f3 /. c)) + ((f2 /. c) * (f3 /. c))
.= ((f1 (#) f3) /. c) + ((f2 /. c) * (f3 /. c)) by A4, Th3
.= ((f1 (#) f3) /. c) + ((f2 (#) f3) /. c) by A6, Th3
.= ((f1 (#) f3) + (f2 (#) f3)) /. c by A1, A2, Th1 ; ::_thesis: verum
end;
hence  (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:16
for C being non empty set
for f3, f1, f2 being PartFunc of C,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by Th15;

theorem Th17: :: CFUNCT_1:17
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2
let r be Element of COMPLEX ; ::_thesis: r (#) (f1 (#) f2) = (r (#) f1) (#) f2
A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by Th4
.= (dom f1) /\ (dom f2) by Th3
.= (dom (r (#) f1)) /\ (dom f2) by Th4
.= dom ((r (#) f1) (#) f2) by Th3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_
(r_(#)_(f1_(#)_f2))_/._c_=_((r_(#)_f1)_(#)_f2)_/._c
let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) /. c = ((r (#) f1) (#) f2) /. c )
assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) /. c = ((r (#) f1) (#) f2) /. c
then A3: c in dom (f1 (#) f2) by Th4;
 c in (dom (r (#) f1)) /\ (dom f2) by A1, A2, Th3;
then A4: c in dom (r (#) f1) by XBOOLE_0:def_4;
thus (r (#) (f1 (#) f2)) /. c = r * ((f1 (#) f2) /. c) by A2, Th4
.= r * ((f1 /. c) * (f2 /. c)) by A3, Th3
.= (r * (f1 /. c)) * (f2 /. c)
.= ((r (#) f1) /. c) * (f2 /. c) by A4, Th4
.= ((r (#) f1) (#) f2) /. c by A1, A2, Th3 ; ::_thesis: verum
end;
hence  r (#) (f1 (#) f2) = (r (#) f1) (#) f2 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th18: :: CFUNCT_1:18
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
let r be Element of COMPLEX ; ::_thesis: r (#) (f1 (#) f2) = f1 (#) (r (#) f2)
A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by Th4
.= (dom f1) /\ (dom f2) by Th3
.= (dom f1) /\ (dom (r (#) f2)) by Th4
.= dom (f1 (#) (r (#) f2)) by Th3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_
(r_(#)_(f1_(#)_f2))_/._c_=_(f1_(#)_(r_(#)_f2))_/._c
let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) /. c = (f1 (#) (r (#) f2)) /. c )
assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) /. c = (f1 (#) (r (#) f2)) /. c
then A3: c in dom (f1 (#) f2) by Th4;
 c in (dom f1) /\ (dom (r (#) f2)) by A1, A2, Th3;
then A4: c in dom (r (#) f2) by XBOOLE_0:def_4;
thus (r (#) (f1 (#) f2)) /. c = r * ((f1 (#) f2) /. c) by A2, Th4
.= r * ((f1 /. c) * (f2 /. c)) by A3, Th3
.= (f1 /. c) * (r * (f2 /. c))
.= (f1 /. c) * ((r (#) f2) /. c) by A4, Th4
.= (f1 (#) (r (#) f2)) /. c by A1, A2, Th3 ; ::_thesis: verum
end;
hence  r (#) (f1 (#) f2) = f1 (#) (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th19: :: CFUNCT_1:19
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
proof
let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
A1: dom ((f1 - f2) (#) f3) = (dom (f1 - f2)) /\ (dom f3) by Th3
.= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by Th2
.= (((dom f1) /\ (dom f2)) /\ (dom f3)) /\ (dom f3) by XBOOLE_1:16
.= (((dom f1) /\ (dom f3)) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= ((dom f1) /\ (dom f3)) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16
.= (dom (f1 (#) f3)) /\ ((dom f2) /\ (dom f3)) by Th3
.= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Th3
.= dom ((f1 (#) f3) - (f2 (#) f3)) by Th2 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_-_f2)_(#)_f3)_holds_
((f1_-_f2)_(#)_f3)_/._c_=_((f1_(#)_f3)_-_(f2_(#)_f3))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 - f2) (#) f3) implies ((f1 - f2) (#) f3) /. c = ((f1 (#) f3) - (f2 (#) f3)) /. c )
assume A2: c in dom ((f1 - f2) (#) f3) ; ::_thesis: ((f1 - f2) (#) f3) /. c = ((f1 (#) f3) - (f2 (#) f3)) /. c
then  c in (dom (f1 - f2)) /\ (dom f3) by Th3;
then A3: c in dom (f1 - f2) by XBOOLE_0:def_4;
A4: c in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, A2, Th2;
then A5: c in dom (f1 (#) f3) by XBOOLE_0:def_4;
A6: c in dom (f2 (#) f3) by A4, XBOOLE_0:def_4;
thus ((f1 - f2) (#) f3) /. c = ((f1 - f2) /. c) * (f3 /. c) by A2, Th3
.= ((f1 /. c) - (f2 /. c)) * (f3 /. c) by A3, Th2
.= ((f1 /. c) * (f3 /. c)) - ((f2 /. c) * (f3 /. c))
.= ((f1 (#) f3) /. c) - ((f2 /. c) * (f3 /. c)) by A5, Th3
.= ((f1 (#) f3) /. c) - ((f2 (#) f3) /. c) by A6, Th3
.= ((f1 (#) f3) - (f2 (#) f3)) /. c by A1, A2, Th2 ; ::_thesis: verum
end;
hence  (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:20
for C being non empty set
for f3, f1, f2 being PartFunc of C,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by Th19;

theorem :: CFUNCT_1:21
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
let r be Element of COMPLEX ; ::_thesis: r (#) (f1 + f2) = (r (#) f1) + (r (#) f2)
A1: dom (r (#) (f1 + f2)) = dom (f1 + f2) by Th4
.= (dom f1) /\ (dom f2) by VALUED_1:def_1
.= (dom f1) /\ (dom (r (#) f2)) by Th4
.= (dom (r (#) f1)) /\ (dom (r (#) f2)) by Th4
.= dom ((r (#) f1) + (r (#) f2)) by VALUED_1:def_1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_+_f2))_holds_
(r_(#)_(f1_+_f2))_/._c_=_((r_(#)_f1)_+_(r_(#)_f2))_/._c
let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 + f2)) implies (r (#) (f1 + f2)) /. c = ((r (#) f1) + (r (#) f2)) /. c )
assume A2: c in dom (r (#) (f1 + f2)) ; ::_thesis: (r (#) (f1 + f2)) /. c = ((r (#) f1) + (r (#) f2)) /. c
then A3: c in dom (f1 + f2) by Th4;
A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, VALUED_1:def_1;
then A5: c in dom (r (#) f1) by XBOOLE_0:def_4;
A6: c in dom (r (#) f2) by A4, XBOOLE_0:def_4;
thus (r (#) (f1 + f2)) /. c = r * ((f1 + f2) /. c) by A2, Th4
.= r * ((f1 /. c) + (f2 /. c)) by A3, Th1
.= (r * (f1 /. c)) + (r * (f2 /. c))
.= ((r (#) f1) /. c) + (r * (f2 /. c)) by A5, Th4
.= ((r (#) f1) /. c) + ((r (#) f2) /. c) by A6, Th4
.= ((r (#) f1) + (r (#) f2)) /. c by A1, A2, Th1 ; ::_thesis: verum
end;
hence  r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:22
for C being non empty set
for f being PartFunc of C,COMPLEX
for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f)
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f)
let f be PartFunc of C,COMPLEX; ::_thesis: for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f)
let r, q be Element of COMPLEX ; ::_thesis: (r * q) (#) f = r (#) (q (#) f)
A1: dom ((r * q) (#) f) = dom f by Th4
.= dom (q (#) f) by Th4
.= dom (r (#) (q (#) f)) by Th4 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_*_q)_(#)_f)_holds_
((r_*_q)_(#)_f)_/._c_=_(r_(#)_(q_(#)_f))_/._c
let c be Element of C; ::_thesis: ( c in dom ((r * q) (#) f) implies ((r * q) (#) f) /. c = (r (#) (q (#) f)) /. c )
assume A2: c in dom ((r * q) (#) f) ; ::_thesis: ((r * q) (#) f) /. c = (r (#) (q (#) f)) /. c
then A3: c in dom (q (#) f) by A1, Th4;
thus ((r * q) (#) f) /. c = (r * q) * (f /. c) by A2, Th4
.= r * (q * (f /. c))
.= r * ((q (#) f) /. c) by A3, Th4
.= (r (#) (q (#) f)) /. c by A1, A2, Th4 ; ::_thesis: verum
end;
hence  (r * q) (#) f = r (#) (q (#) f) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:23
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
let r be Element of COMPLEX ; ::_thesis: r (#) (f1 - f2) = (r (#) f1) - (r (#) f2)
A1: dom (r (#) (f1 - f2)) = dom (f1 - f2) by Th4
.= (dom f1) /\ (dom f2) by Th2
.= (dom f1) /\ (dom (r (#) f2)) by Th4
.= (dom (r (#) f1)) /\ (dom (r (#) f2)) by Th4
.= dom ((r (#) f1) - (r (#) f2)) by Th2 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_-_f2))_holds_
(r_(#)_(f1_-_f2))_/._c_=_((r_(#)_f1)_-_(r_(#)_f2))_/._c
let c be Element of C; ::_thesis: ( c in dom (r (#) (f1 - f2)) implies (r (#) (f1 - f2)) /. c = ((r (#) f1) - (r (#) f2)) /. c )
assume A2: c in dom (r (#) (f1 - f2)) ; ::_thesis: (r (#) (f1 - f2)) /. c = ((r (#) f1) - (r (#) f2)) /. c
then A3: c in dom (f1 - f2) by Th4;
A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, Th2;
then A5: c in dom (r (#) f1) by XBOOLE_0:def_4;
A6: c in dom (r (#) f2) by A4, XBOOLE_0:def_4;
thus (r (#) (f1 - f2)) /. c = r * ((f1 - f2) /. c) by A2, Th4
.= r * ((f1 /. c) - (f2 /. c)) by A3, Th2
.= (r * (f1 /. c)) - (r * (f2 /. c))
.= ((r (#) f1) /. c) - (r * (f2 /. c)) by A5, Th4
.= ((r (#) f1) /. c) - ((r (#) f2) /. c) by A6, Th4
.= ((r (#) f1) - (r (#) f2)) /. c by A1, A2, Th2 ; ::_thesis: verum
end;
hence  r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:24
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds f1 - f2 = (- 1r) (#) (f2 - f1)
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds f1 - f2 = (- 1r) (#) (f2 - f1)
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: f1 - f2 = (- 1r) (#) (f2 - f1)
A1: dom (f1 - f2) = (dom f2) /\ (dom f1) by Th2
.= dom (f2 - f1) by Th2
.= dom ((- 1r) (#) (f2 - f1)) by Th4 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_f2)_holds_
(f1_-_f2)_/._c_=_((-_1r)_(#)_(f2_-_f1))_/._c
A2: dom (f1 - f2) = (dom f2) /\ (dom f1) by Th2
.= dom (f2 - f1) by Th2 ;
let c be Element of C; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) /. c = ((- 1r) (#) (f2 - f1)) /. c )
assume A3: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) /. c = ((- 1r) (#) (f2 - f1)) /. c
thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A3, Th2
.= (- 1) * ((f2 /. c) - (f1 /. c))
.= (- 1r) * ((f2 - f1) /. c) by A3, A2, Th2, COMPLEX1:def_4
.= ((- 1r) (#) (f2 - f1)) /. c by A1, A3, Th4 ; ::_thesis: verum
end;
hence  f1 - f2 = (- 1r) (#) (f2 - f1) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:25
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 + f3) = (f1 - f2) - f3
proof
let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 + f3) = (f1 - f2) - f3
let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: f1 - (f2 + f3) = (f1 - f2) - f3
A1: dom (f1 - (f2 + f3)) = (dom f1) /\ (dom (f2 + f3)) by Th2
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VALUED_1:def_1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by Th2
.= dom ((f1 - f2) - f3) by Th2 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_(f2_+_f3))_holds_
(f1_-_(f2_+_f3))_/._c_=_((f1_-_f2)_-_f3)_/._c
let c be Element of C; ::_thesis: ( c in dom (f1 - (f2 + f3)) implies (f1 - (f2 + f3)) /. c = ((f1 - f2) - f3) /. c )
assume A2: c in dom (f1 - (f2 + f3)) ; ::_thesis: (f1 - (f2 + f3)) /. c = ((f1 - f2) - f3) /. c
then  c in (dom f1) /\ (dom (f2 + f3)) by Th2;
then A3: c in dom (f2 + f3) by XBOOLE_0:def_4;
 c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, Th2;
then A4: c in dom (f1 - f2) by XBOOLE_0:def_4;
thus (f1 - (f2 + f3)) /. c = (f1 /. c) - ((f2 + f3) /. c) by A2, Th2
.= (f1 /. c) - ((f2 /. c) + (f3 /. c)) by A3, Th1
.= ((f1 /. c) - (f2 /. c)) - (f3 /. c)
.= ((f1 - f2) /. c) - (f3 /. c) by A4, Th2
.= ((f1 - f2) - f3) /. c by A1, A2, Th2 ; ::_thesis: verum
end;
hence  f1 - (f2 + f3) = (f1 - f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:26
for C being non empty set
for f being PartFunc of C,COMPLEX holds 1r (#) f = f
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds 1r (#) f = f
let f be PartFunc of C,COMPLEX; ::_thesis: 1r (#) f = f
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(1r_(#)_f)_holds_
(1r_(#)_f)_/._c_=_f_/._c
let c be Element of C; ::_thesis: ( c in dom (1r (#) f) implies (1r (#) f) /. c = f /. c )
assume  c in dom (1r (#) f) ; ::_thesis: (1r (#) f) /. c = f /. c
hence (1r (#) f) /. c = 1r * (f /. c) by Th4
.= f /. c by COMPLEX1:def_4 ;
::_thesis: verum
end;
 dom (1r (#) f) = dom f by Th4;
hence  1r (#) f = f by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:27
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 - f3) = (f1 - f2) + f3
proof
let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 - f3) = (f1 - f2) + f3
let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: f1 - (f2 - f3) = (f1 - f2) + f3
A1: dom (f1 - (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by Th2
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by Th2
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by Th2
.= dom ((f1 - f2) + f3) by VALUED_1:def_1 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_(f2_-_f3))_holds_
(f1_-_(f2_-_f3))_/._c_=_((f1_-_f2)_+_f3)_/._c
let c be Element of C; ::_thesis: ( c in dom (f1 - (f2 - f3)) implies (f1 - (f2 - f3)) /. c = ((f1 - f2) + f3) /. c )
assume A2: c in dom (f1 - (f2 - f3)) ; ::_thesis: (f1 - (f2 - f3)) /. c = ((f1 - f2) + f3) /. c
then  c in (dom (f1 - f2)) /\ (dom f3) by A1, VALUED_1:def_1;
then A3: c in dom (f1 - f2) by XBOOLE_0:def_4;
 c in (dom f1) /\ (dom (f2 - f3)) by A2, Th2;
then A4: c in dom (f2 - f3) by XBOOLE_0:def_4;
thus (f1 - (f2 - f3)) /. c = (f1 /. c) - ((f2 - f3) /. c) by A2, Th2
.= (f1 /. c) - ((f2 /. c) - (f3 /. c)) by A4, Th2
.= ((f1 /. c) - (f2 /. c)) + (f3 /. c)
.= ((f1 - f2) /. c) + (f3 /. c) by A3, Th2
.= ((f1 - f2) + f3) /. c by A1, A2, Th1 ; ::_thesis: verum
end;
hence  f1 - (f2 - f3) = (f1 - f2) + f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:28
for C being non empty set
for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 + (f2 - f3) = (f1 + f2) - f3
proof
let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 + (f2 - f3) = (f1 + f2) - f3
let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: f1 + (f2 - f3) = (f1 + f2) - f3
A1: dom (f1 + (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by VALUED_1:def_1
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by Th2
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1
.= dom ((f1 + f2) - f3) by Th2 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_(f2_-_f3))_holds_
(f1_+_(f2_-_f3))_/._c_=_((f1_+_f2)_-_f3)_/._c
let c be Element of C; ::_thesis: ( c in dom (f1 + (f2 - f3)) implies (f1 + (f2 - f3)) /. c = ((f1 + f2) - f3) /. c )
assume A2: c in dom (f1 + (f2 - f3)) ; ::_thesis: (f1 + (f2 - f3)) /. c = ((f1 + f2) - f3) /. c
then  c in (dom f1) /\ (dom (f2 - f3)) by VALUED_1:def_1;
then A3: c in dom (f2 - f3) by XBOOLE_0:def_4;
 c in (dom (f1 + f2)) /\ (dom f3) by A1, A2, Th2;
then A4: c in dom (f1 + f2) by XBOOLE_0:def_4;
thus (f1 + (f2 - f3)) /. c = (f1 /. c) + ((f2 - f3) /. c) by A2, Th1
.= (f1 /. c) + ((f2 /. c) - (f3 /. c)) by A3, Th2
.= ((f1 /. c) + (f2 /. c)) - (f3 /. c)
.= ((f1 + f2) /. c) - (f3 /. c) by A4, Th1
.= ((f1 + f2) - f3) /. c by A1, A2, Th2 ; ::_thesis: verum
end;
hence  f1 + (f2 - f3) = (f1 + f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th29: :: CFUNCT_1:29
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 (#) f2).| = |.f1.| (#) |.f2.|
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 (#) f2).| = |.f1.| (#) |.f2.|
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: |.(f1 (#) f2).| = |.f1.| (#) |.f2.|
A1: dom |.(f1 (#) f2).| = dom (f1 (#) f2) by VALUED_1:def_11
.= (dom f1) /\ (dom f2) by Th3
.= (dom f1) /\ (dom |.f2.|) by VALUED_1:def_11
.= (dom |.f1.|) /\ (dom |.f2.|) by VALUED_1:def_11
.= dom (|.f1.| (#) |.f2.|) by VALUED_1:def_4 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_|.(f1_(#)_f2).|_holds_
|.(f1_(#)_f2).|_._c_=_(|.f1.|_(#)_|.f2.|)_._c
A2: dom |.f2.| = dom f2 by VALUED_1:def_11;
let c be Element of C; ::_thesis: ( c in dom |.(f1 (#) f2).| implies |.(f1 (#) f2).| . c = (|.f1.| (#) |.f2.|) . c )
A3: dom |.f1.| = dom f1 by VALUED_1:def_11;
assume A4: c in dom |.(f1 (#) f2).| ; ::_thesis: |.(f1 (#) f2).| . c = (|.f1.| (#) |.f2.|) . c
then A5: c in dom (f1 (#) f2) by VALUED_1:def_11;
A6: c in (dom |.f1.|) /\ (dom |.f2.|) by A1, A4, VALUED_1:def_4;
then  c in dom |.f1.| by XBOOLE_0:def_4;
then A7: f1 . c = f1 /. c by A3, PARTFUN1:def_6;
 c in dom |.f2.| by A6, XBOOLE_0:def_4;
then A8: f2 /. c = f2 . c by A2, PARTFUN1:def_6;
thus |.(f1 (#) f2).| . c = |.((f1 (#) f2) . c).| by VALUED_1:18
.= |.((f1 (#) f2) /. c).| by A5, PARTFUN1:def_6
.= |.((f1 /. c) * (f2 /. c)).| by A5, Th3
.= |.(f1 /. c).| * |.(f2 /. c).| by COMPLEX1:65
.= (|.f1.| . c) * |.(f2 /. c).| by A7, VALUED_1:18
.= (|.f1.| . c) * (|.f2.| . c) by A8, VALUED_1:18
.= (|.f1.| (#) |.f2.|) . c by VALUED_1:5 ; ::_thesis: verum
end;
hence  |.(f1 (#) f2).| = |.f1.| (#) |.f2.| by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th30: :: CFUNCT_1:30
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.|
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.|
let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.|
let r be Element of COMPLEX ; ::_thesis: |.(r (#) f).| = |.r.| (#) |.f.|
A1: dom f = dom |.f.| by VALUED_1:def_11;
A2: dom |.(r (#) f).| = dom (r (#) f) by VALUED_1:def_11
.= dom f by Th4
.= dom (|.r.| (#) |.f.|) by A1, VALUED_1:def_5 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_|.(r_(#)_f).|_holds_
|.(r_(#)_f).|_._c_=_(|.r.|_(#)_|.f.|)_._c
let c be Element of C; ::_thesis: ( c in dom |.(r (#) f).| implies |.(r (#) f).| . c = (|.r.| (#) |.f.|) . c )
assume A3: c in dom |.(r (#) f).| ; ::_thesis: |.(r (#) f).| . c = (|.r.| (#) |.f.|) . c
then A4: c in dom (r (#) f) by VALUED_1:def_11;
A5: c in dom |.f.| by A2, A3, VALUED_1:def_5;
thus |.(r (#) f).| . c = |.((r (#) f) . c).| by VALUED_1:18
.= |.((r (#) f) /. c).| by A4, PARTFUN1:def_6
.= |.(r * (f /. c)).| by A4, Th4
.= |.r.| * |.(f /. c).| by COMPLEX1:65
.= |.r.| * |.(f . c).| by A1, A5, PARTFUN1:def_6
.= |.r.| * (|.f.| . c) by VALUED_1:18
.= (|.r.| (#) |.f.|) . c by A2, A3, VALUED_1:def_5 ; ::_thesis: verum
end;
hence  |.(r (#) f).| = |.r.| (#) |.f.| by A2, PARTFUN1:5; ::_thesis: verum
end;

theorem :: CFUNCT_1:31
for C being non empty set
for f being PartFunc of C,COMPLEX holds - f = (- 1r) (#) f by COMPLEX1:def_4;

theorem :: CFUNCT_1:32
canceled;

theorem :: CFUNCT_1:33
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds f1 - (- f2) = f1 + f2 ;

theorem Th34: :: CFUNCT_1:34
for C being non empty set
for f being PartFunc of C,COMPLEX holds (f ^) ^ = f | (dom (f ^))
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds (f ^) ^ = f | (dom (f ^))
let f be PartFunc of C,COMPLEX; ::_thesis: (f ^) ^ = f | (dom (f ^))
A1: dom ((f ^) ^) = dom (f | (dom (f ^))) by Th11;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f_^)_^)_holds_
((f_^)_^)_/._c_=_(f_|_(dom_(f_^)))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f ^) ^) implies ((f ^) ^) /. c = (f | (dom (f ^))) /. c )
assume A2: c in dom ((f ^) ^) ; ::_thesis: ((f ^) ^) /. c = (f | (dom (f ^))) /. c
then  c in (dom f) /\ (dom (f ^)) by A1, RELAT_1:61;
then A3: c in dom (f ^) by XBOOLE_0:def_4;
thus ((f ^) ^) /. c = ((f ^) /. c) " by A2, Def2
.= ((f /. c) ") " by A3, Def2
.= (f | (dom (f ^))) /. c by A1, A2, PARTFUN2:15 ; ::_thesis: verum
end;
hence  (f ^) ^ = f | (dom (f ^)) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th35: :: CFUNCT_1:35
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
A1: dom ((f1 (#) f2) ^) = (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0c}) by Def2
.= ((dom f1) \ (f1 " {0c})) /\ ((dom f2) \ (f2 " {0c})) by Th7
.= (dom (f1 ^)) /\ ((dom f2) \ (f2 " {0c})) by Def2
.= (dom (f1 ^)) /\ (dom (f2 ^)) by Def2
.= dom ((f1 ^) (#) (f2 ^)) by Th3 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_^)_holds_
((f1_(#)_f2)_^)_/._c_=_((f1_^)_(#)_(f2_^))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) ^) implies ((f1 (#) f2) ^) /. c = ((f1 ^) (#) (f2 ^)) /. c )
assume A2: c in dom ((f1 (#) f2) ^) ; ::_thesis: ((f1 (#) f2) ^) /. c = ((f1 ^) (#) (f2 ^)) /. c
then  c in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0c}) by Def2;
then A3: c in dom (f1 (#) f2) by XBOOLE_0:def_5;
A4: c in (dom (f1 ^)) /\ (dom (f2 ^)) by A1, A2, Th3;
then A5: c in dom (f1 ^) by XBOOLE_0:def_4;
A6: c in dom (f2 ^) by A4, XBOOLE_0:def_4;
thus ((f1 (#) f2) ^) /. c = ((f1 (#) f2) /. c) " by A2, Def2
.= ((f1 /. c) * (f2 /. c)) " by A3, Th3
.= ((f1 /. c) ") * ((f2 /. c) ") by XCMPLX_1:204
.= ((f1 ^) /. c) * ((f2 /. c) ") by A5, Def2
.= ((f1 ^) /. c) * ((f2 ^) /. c) by A6, Def2
.= ((f1 ^) (#) (f2 ^)) /. c by A1, A2, Th3 ; ::_thesis: verum
end;
hence  (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th36: :: CFUNCT_1:36
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st r <> 0 holds
(r (#) f) ^ = (r ") (#) (f ^)
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st r <> 0 holds
(r (#) f) ^ = (r ") (#) (f ^)
let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX st r <> 0 holds
(r (#) f) ^ = (r ") (#) (f ^)
let r be Element of COMPLEX ; ::_thesis: ( r <> 0 implies (r (#) f) ^ = (r ") (#) (f ^) )
assume A1: r <> 0 ; ::_thesis: (r (#) f) ^ = (r ") (#) (f ^)
A2: dom ((r (#) f) ^) = (dom (r (#) f)) \ ((r (#) f) " {0c}) by Def2
.= (dom (r (#) f)) \ (f " {0c}) by A1, Th12
.= (dom f) \ (f " {0c}) by Th4
.= dom (f ^) by Def2
.= dom ((r ") (#) (f ^)) by Th4 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_(#)_f)_^)_holds_
((r_(#)_f)_^)_/._c_=_((r_")_(#)_(f_^))_/._c
let c be Element of C; ::_thesis: ( c in dom ((r (#) f) ^) implies ((r (#) f) ^) /. c = ((r ") (#) (f ^)) /. c )
assume A3: c in dom ((r (#) f) ^) ; ::_thesis: ((r (#) f) ^) /. c = ((r ") (#) (f ^)) /. c
then A4: c in dom (f ^) by A2, Th4;
 c in (dom (r (#) f)) \ ((r (#) f) " {0c}) by A3, Def2;
then A5: c in dom (r (#) f) by XBOOLE_0:def_5;
thus ((r (#) f) ^) /. c = ((r (#) f) /. c) " by A3, Def2
.= (r * (f /. c)) " by A5, Th4
.= (r ") * ((f /. c) ") by XCMPLX_1:204
.= (r ") * ((f ^) /. c) by A4, Def2
.= ((r ") (#) (f ^)) /. c by A2, A3, Th4 ; ::_thesis: verum
end;
hence  (r (#) f) ^ = (r ") (#) (f ^) by A2, PARTFUN2:1; ::_thesis: verum
end;

Lm2:  (- 1r) " = - 1r
by COMPLEX1:def_4;

theorem :: CFUNCT_1:37
for C being non empty set
for f being PartFunc of C,COMPLEX holds (- f) ^ = (- 1r) (#) (f ^) by Lm2, Th36, COMPLEX1:def_4;

theorem Th38: :: CFUNCT_1:38
for C being non empty set
for f being PartFunc of C,COMPLEX holds |.f.| ^ = |.(f ^).|
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds |.f.| ^ = |.(f ^).|
let f be PartFunc of C,COMPLEX; ::_thesis: |.f.| ^ = |.(f ^).|
A1: dom (|.f.| ^) = (dom |.f.|) \ (|.f.| " {0}) by RFUNCT_1:def_2
.= (dom f) \ (|.f.| " {0}) by VALUED_1:def_11
.= (dom f) \ (f " {0c}) by Th10
.= dom (f ^) by Def2
.= dom |.(f ^).| by VALUED_1:def_11 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(|.f.|_^)_holds_
(|.f.|_^)_._c_=_|.(f_^).|_._c
let c be Element of C; ::_thesis: ( c in dom (|.f.| ^) implies (|.f.| ^) . c = |.(f ^).| . c )
A2: dom f = dom |.f.| by VALUED_1:def_11;
assume A3: c in dom (|.f.| ^) ; ::_thesis: (|.f.| ^) . c = |.(f ^).| . c
then A4: c in dom (f ^) by A1, VALUED_1:def_11;
 c in (dom |.f.|) \ (|.f.| " {0}) by A3, RFUNCT_1:def_2;
then A5: c in dom |.f.| by XBOOLE_0:def_5;
thus (|.f.| ^) . c = (|.f.| . c) " by A3, RFUNCT_1:def_2
.= |.(f . c).| " by VALUED_1:18
.= |.(f /. c).| " by A5, A2, PARTFUN1:def_6
.= |.1r.| / |.(f /. c).| by COMPLEX1:48, XCMPLX_1:215
.= |.(1r / (f /. c)).| by COMPLEX1:67
.= |.((f /. c) ").| by COMPLEX1:def_4, XCMPLX_1:215
.= |.((f ^) /. c).| by A4, Def2
.= |.((f ^) . c).| by A4, PARTFUN1:def_6
.= |.(f ^).| . c by VALUED_1:18 ; ::_thesis: verum
end;
hence  |.f.| ^ = |.(f ^).| by A1, PARTFUN1:5; ::_thesis: verum
end;

theorem Th39: :: CFUNCT_1:39
for C being non empty set
for f, g being PartFunc of C,COMPLEX holds f / g = f (#) (g ^)
proof
let C be non empty set ; ::_thesis: for f, g being PartFunc of C,COMPLEX holds f / g = f (#) (g ^)
let f, g be PartFunc of C,COMPLEX; ::_thesis: f / g = f (#) (g ^)
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f_/_g)_holds_
(f_/_g)_/._c_=_(f_(#)_(g_^))_/._c
let c be Element of C; ::_thesis: ( c in dom (f / g) implies (f / g) /. c = (f (#) (g ^)) /. c )
assume A2: c in dom (f / g) ; ::_thesis: (f / g) /. c = (f (#) (g ^)) /. c
then  c in (dom f) /\ ((dom g) \ (g " {0c})) by Def1;
then A3: c in (dom f) /\ (dom (g ^)) by Def2;
then A4: c in dom (g ^) by XBOOLE_0:def_4;
A5: c in dom (f (#) (g ^)) by A3, Th3;
thus (f / g) /. c = (f /. c) * ((g /. c) ") by A2, Def1
.= (f /. c) * ((g ^) /. c) by A4, Def2
.= (f (#) (g ^)) /. c by A5, Th3 ; ::_thesis: verum
end;
dom (f / g) = (dom f) /\ ((dom g) \ (g " {0c})) by Def1
.= (dom f) /\ (dom (g ^)) by Def2
.= dom (f (#) (g ^)) by Th3 ;
hence  f / g = f (#) (g ^) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th40: :: CFUNCT_1:40
for C being non empty set
for g, f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f
proof
let C be non empty set ; ::_thesis: for g, f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f
let g, f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f
let r be Element of COMPLEX ; ::_thesis: r (#) (g / f) = (r (#) g) / f
thus r (#) (g / f) = r (#) (g (#) (f ^)) by Th39
.= (r (#) g) (#) (f ^) by Th17
.= (r (#) g) / f by Th39 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:41
for C being non empty set
for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^))
proof
let C be non empty set ; ::_thesis: for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^))
let f, g be PartFunc of C,COMPLEX; ::_thesis: (f / g) (#) g = f | (dom (g ^))
A1: dom ((f / g) (#) g) = (dom (f / g)) /\ (dom g) by Th3
.= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ (dom g) by Def1
.= (dom f) /\ (((dom g) \ (g " {0c})) /\ (dom g)) by XBOOLE_1:16
.= (dom f) /\ ((dom (g ^)) /\ (dom g)) by Def2
.= (dom f) /\ (dom (g ^)) by Th6, XBOOLE_1:28
.= dom (f | (dom (g ^))) by RELAT_1:61 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f_/_g)_(#)_g)_holds_
((f_/_g)_(#)_g)_/._c_=_(f_|_(dom_(g_^)))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f / g) (#) g) implies ((f / g) (#) g) /. c = (f | (dom (g ^))) /. c )
assume A2: c in dom ((f / g) (#) g) ; ::_thesis: ((f / g) (#) g) /. c = (f | (dom (g ^))) /. c
then A3: c in (dom f) /\ (dom (g ^)) by A1, RELAT_1:61;
then A4: c in dom (f (#) (g ^)) by Th3;
A5: c in dom (g ^) by A3, XBOOLE_0:def_4;
then A6: g /. c <> 0c by Th8;
thus ((f / g) (#) g) /. c = ((f / g) /. c) * (g /. c) by A2, Th3
.= ((f (#) (g ^)) /. c) * (g /. c) by Th39
.= ((f /. c) * ((g ^) /. c)) * (g /. c) by A4, Th3
.= ((f /. c) * ((g /. c) ")) * (g /. c) by A5, Def2
.= (f /. c) * (((g /. c) ") * (g /. c))
.= (f /. c) * 1r by A6, COMPLEX1:def_4, XCMPLX_0:def_7
.= (f | (dom (g ^))) /. c by A1, A2, COMPLEX1:def_4, PARTFUN2:15 ; ::_thesis: verum
end;
hence  (f / g) (#) g = f | (dom (g ^)) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th42: :: CFUNCT_1:42
for C being non empty set
for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
proof
let C be non empty set ; ::_thesis: for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
let f, g, f1, g1 be PartFunc of C,COMPLEX; ::_thesis: (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1)
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f_/_g)_(#)_(f1_/_g1))_holds_
((f_/_g)_(#)_(f1_/_g1))_/._c_=_((f_(#)_f1)_/_(g_(#)_g1))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f / g) (#) (f1 / g1)) implies ((f / g) (#) (f1 / g1)) /. c = ((f (#) f1) / (g (#) g1)) /. c )
assume A2: c in dom ((f / g) (#) (f1 / g1)) ; ::_thesis: ((f / g) (#) (f1 / g1)) /. c = ((f (#) f1) / (g (#) g1)) /. c
then  c in (dom (f / g)) /\ (dom (f1 / g1)) by Th3;
then A3: c in (dom (f (#) (g ^))) /\ (dom (f1 / g1)) by Th39;
then A4: c in dom (f (#) (g ^)) by XBOOLE_0:def_4;
then A5: c in (dom f) /\ (dom (g ^)) by Th3;
 c in (dom (f (#) (g ^))) /\ (dom (f1 (#) (g1 ^))) by A3, Th39;
then A6: c in dom (f1 (#) (g1 ^)) by XBOOLE_0:def_4;
then A7: c in (dom f1) /\ (dom (g1 ^)) by Th3;
then A8: c in dom f1 by XBOOLE_0:def_4;
 c in dom f by A5, XBOOLE_0:def_4;
then  c in (dom f) /\ (dom f1) by A8, XBOOLE_0:def_4;
then A9: c in dom (f (#) f1) by Th3;
A10: c in dom (g1 ^) by A7, XBOOLE_0:def_4;
 c in dom (g ^) by A5, XBOOLE_0:def_4;
then  c in (dom (g ^)) /\ (dom (g1 ^)) by A10, XBOOLE_0:def_4;
then A11: c in dom ((g ^) (#) (g1 ^)) by Th3;
then  c in dom ((g (#) g1) ^) by Th35;
then  c in (dom (f (#) f1)) /\ (dom ((g (#) g1) ^)) by A9, XBOOLE_0:def_4;
then A12: c in dom ((f (#) f1) (#) ((g (#) g1) ^)) by Th3;
thus ((f / g) (#) (f1 / g1)) /. c = ((f / g) /. c) * ((f1 / g1) /. c) by A2, Th3
.= ((f (#) (g ^)) /. c) * ((f1 / g1) /. c) by Th39
.= ((f (#) (g ^)) /. c) * ((f1 (#) (g1 ^)) /. c) by Th39
.= ((f /. c) * ((g ^) /. c)) * ((f1 (#) (g1 ^)) /. c) by A4, Th3
.= ((f /. c) * ((g ^) /. c)) * ((f1 /. c) * ((g1 ^) /. c)) by A6, Th3
.= (f /. c) * ((f1 /. c) * (((g ^) /. c) * ((g1 ^) /. c)))
.= (f /. c) * ((f1 /. c) * (((g ^) (#) (g1 ^)) /. c)) by A11, Th3
.= ((f /. c) * (f1 /. c)) * (((g ^) (#) (g1 ^)) /. c)
.= ((f /. c) * (f1 /. c)) * (((g (#) g1) ^) /. c) by Th35
.= ((f (#) f1) /. c) * (((g (#) g1) ^) /. c) by A9, Th3
.= ((f (#) f1) (#) ((g (#) g1) ^)) /. c by A12, Th3
.= ((f (#) f1) / (g (#) g1)) /. c by Th39 ; ::_thesis: verum
end;
dom ((f / g) (#) (f1 / g1)) = (dom (f / g)) /\ (dom (f1 / g1)) by Th3
.= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ (dom (f1 / g1)) by Def1
.= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0c}))) by Def1
.= (dom f) /\ (((dom g) \ (g " {0c})) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0c})))) by XBOOLE_1:16
.= (dom f) /\ ((dom f1) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c})))) by XBOOLE_1:16
.= ((dom f) /\ (dom f1)) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c}))) by XBOOLE_1:16
.= (dom (f (#) f1)) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c}))) by Th3
.= (dom (f (#) f1)) /\ ((dom (g (#) g1)) \ ((g (#) g1) " {0c})) by Th7
.= dom ((f (#) f1) / (g (#) g1)) by Def1 ;
hence  (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem Th43: :: CFUNCT_1:43
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1
thus (f1 / f2) ^ = (f1 (#) (f2 ^)) ^ by Th39
.= (f1 ^) (#) ((f2 ^) ^) by Th35
.= (f2 | (dom (f2 ^))) (#) (f1 ^) by Th34
.= (f2 | (dom (f2 ^))) / f1 by Th39 ; ::_thesis: verum
end;

theorem Th44: :: CFUNCT_1:44
for C being non empty set
for g, f1, f2 being PartFunc of C,COMPLEX holds g (#) (f1 / f2) = (g (#) f1) / f2
proof
let C be non empty set ; ::_thesis: for g, f1, f2 being PartFunc of C,COMPLEX holds g (#) (f1 / f2) = (g (#) f1) / f2
let g, f1, f2 be PartFunc of C,COMPLEX; ::_thesis: g (#) (f1 / f2) = (g (#) f1) / f2
thus g (#) (f1 / f2) = g (#) (f1 (#) (f2 ^)) by Th39
.= (g (#) f1) (#) (f2 ^) by Th14
.= (g (#) f1) / f2 by Th39 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:45
for C being non empty set
for g, f1, f2 being PartFunc of C,COMPLEX holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1
proof
let C be non empty set ; ::_thesis: for g, f1, f2 being PartFunc of C,COMPLEX holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1
let g, f1, f2 be PartFunc of C,COMPLEX; ::_thesis: g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1
thus g / (f1 / f2) = g (#) ((f1 / f2) ^) by Th39
.= g (#) ((f2 | (dom (f2 ^))) / f1) by Th43
.= (g (#) (f2 | (dom (f2 ^)))) / f1 by Th44 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:46
for C being non empty set
for f, g being PartFunc of C,COMPLEX holds
( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
proof
let C be non empty set ; ::_thesis: for f, g being PartFunc of C,COMPLEX holds
( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
let f, g be PartFunc of C,COMPLEX; ::_thesis: ( - (f / g) = (- f) / g & f / (- g) = - (f / g) )
thus  - (f / g) = (- 1r) (#) (f / g) by COMPLEX1:def_4
.= (- f) / g by Th40, COMPLEX1:def_4 ; ::_thesis: f / (- g) = - (f / g)
thus f / (- g) = f (#) ((- g) ^) by Th39
.= f (#) ((- 1r) (#) (g ^)) by Lm2, Th36, COMPLEX1:def_4
.= - (f (#) (g ^)) by Th18, COMPLEX1:def_4
.= - (f / g) by Th39 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:47
for C being non empty set
for f1, f, f2 being PartFunc of C,COMPLEX holds
( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
proof
let C be non empty set ; ::_thesis: for f1, f, f2 being PartFunc of C,COMPLEX holds
( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
let f1, f, f2 be PartFunc of C,COMPLEX; ::_thesis: ( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f )
thus (f1 / f) + (f2 / f) = (f1 (#) (f ^)) + (f2 / f) by Th39
.= (f1 (#) (f ^)) + (f2 (#) (f ^)) by Th39
.= (f1 + f2) (#) (f ^) by Th15
.= (f1 + f2) / f by Th39 ; ::_thesis: (f1 / f) - (f2 / f) = (f1 - f2) / f
thus (f1 / f) - (f2 / f) = (f1 (#) (f ^)) - (f2 / f) by Th39
.= (f1 (#) (f ^)) - (f2 (#) (f ^)) by Th39
.= (f1 - f2) (#) (f ^) by Th19
.= (f1 - f2) / f by Th39 ; ::_thesis: verum
end;

theorem Th48: :: CFUNCT_1:48
for C being non empty set
for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
proof
let C be non empty set ; ::_thesis: for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
let f1, f, g1, g be PartFunc of C,COMPLEX; ::_thesis: (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g)
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_/_f)_+_(g1_/_g))_holds_
((f1_/_f)_+_(g1_/_g))_/._c_=_(((f1_(#)_g)_+_(g1_(#)_f))_/_(f_(#)_g))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 / f) + (g1 / g)) implies ((f1 / f) + (g1 / g)) /. c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c )
A2: dom (f ^) c= dom f by Th6;
assume A3: c in dom ((f1 / f) + (g1 / g)) ; ::_thesis: ((f1 / f) + (g1 / g)) /. c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c
then A4: c in (dom (f1 / f)) /\ (dom (g1 / g)) by VALUED_1:def_1;
then A5: c in dom (f1 / f) by XBOOLE_0:def_4;
A6: c in dom (g1 / g) by A4, XBOOLE_0:def_4;
A7: c in (dom (f1 (#) (f ^))) /\ (dom (g1 / g)) by A4, Th39;
then  c in dom (f1 (#) (f ^)) by XBOOLE_0:def_4;
then A8: c in (dom f1) /\ (dom (f ^)) by Th3;
then A9: c in dom (f ^) by XBOOLE_0:def_4;
then A10: f /. c <> 0c by Th8;
 c in (dom (f1 (#) (f ^))) /\ (dom (g1 (#) (g ^))) by A7, Th39;
then  c in dom (g1 (#) (g ^)) by XBOOLE_0:def_4;
then A11: c in (dom g1) /\ (dom (g ^)) by Th3;
then A12: c in dom (g ^) by XBOOLE_0:def_4;
then A13: g /. c <> 0c by Th8;
 c in dom g1 by A11, XBOOLE_0:def_4;
then  c in (dom g1) /\ (dom f) by A9, A2, XBOOLE_0:def_4;
then A14: c in dom (g1 (#) f) by Th3;
A15: dom (g ^) c= dom g by Th6;
then  c in (dom f) /\ (dom g) by A9, A12, A2, XBOOLE_0:def_4;
then A16: c in dom (f (#) g) by Th3;
 c in dom f1 by A8, XBOOLE_0:def_4;
then  c in (dom f1) /\ (dom g) by A12, A15, XBOOLE_0:def_4;
then A17: c in dom (f1 (#) g) by Th3;
then  c in (dom (f1 (#) g)) /\ (dom (g1 (#) f)) by A14, XBOOLE_0:def_4;
then A18: c in dom ((f1 (#) g) + (g1 (#) f)) by VALUED_1:def_1;
 c in (dom (f ^)) /\ (dom (g ^)) by A9, A12, XBOOLE_0:def_4;
then  c in dom ((f ^) (#) (g ^)) by Th3;
then  c in dom ((f (#) g) ^) by Th35;
then  c in (dom ((f1 (#) g) + (g1 (#) f))) /\ (dom ((f (#) g) ^)) by A18, XBOOLE_0:def_4;
then  c in dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^)) by Th3;
then A19: c in dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Th39;
thus ((f1 / f) + (g1 / g)) /. c = ((f1 / f) /. c) + ((g1 / g) /. c) by A3, Th1
.= ((f1 /. c) * ((f /. c) ")) + ((g1 / g) /. c) by A5, Def1
.= ((f1 /. c) * (1r * ((f /. c) "))) + (((g1 /. c) * 1r) * ((g /. c) ")) by A6, Def1, COMPLEX1:def_4
.= ((f1 /. c) * (((g /. c) * ((g /. c) ")) * ((f /. c) "))) + ((g1 /. c) * (1r * ((g /. c) "))) by A13, COMPLEX1:def_4, XCMPLX_0:def_7
.= ((f1 /. c) * ((g /. c) * (((g /. c) ") * ((f /. c) ")))) + ((g1 /. c) * (((f /. c) * ((f /. c) ")) * ((g /. c) "))) by A10, COMPLEX1:def_4, XCMPLX_0:def_7
.= ((f1 /. c) * ((g /. c) * (((g /. c) * (f /. c)) "))) + ((g1 /. c) * ((f /. c) * (((f /. c) ") * ((g /. c) ")))) by XCMPLX_1:204
.= ((f1 /. c) * ((g /. c) * (((f /. c) * (g /. c)) "))) + ((g1 /. c) * ((f /. c) * (((f /. c) * (g /. c)) "))) by XCMPLX_1:204
.= ((f1 /. c) * ((g /. c) * (((f (#) g) /. c) "))) + ((g1 /. c) * ((f /. c) * (((f /. c) * (g /. c)) "))) by A16, Th3
.= (((f1 /. c) * (g /. c)) * (((f (#) g) /. c) ")) + ((g1 /. c) * ((f /. c) * (((f (#) g) /. c) "))) by A16, Th3
.= (((f1 (#) g) /. c) * (((f (#) g) /. c) ")) + (((g1 /. c) * (f /. c)) * (((f (#) g) /. c) ")) by A17, Th3
.= (((f1 (#) g) /. c) * (((f (#) g) /. c) ")) + (((g1 (#) f) /. c) * (((f (#) g) /. c) ")) by A14, Th3
.= (((f1 (#) g) /. c) + ((g1 (#) f) /. c)) * (((f (#) g) /. c) ")
.= (((f1 (#) g) + (g1 (#) f)) /. c) * (((f (#) g) /. c) ") by A18, Th1
.= (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c by A19, Def1 ; ::_thesis: verum
end;
dom ((f1 / f) + (g1 / g)) = (dom (f1 / f)) /\ (dom (g1 / g)) by VALUED_1:def_1
.= ((dom f1) /\ ((dom f) \ (f " {0c}))) /\ (dom (g1 / g)) by Def1
.= ((dom f1) /\ ((dom f) \ (f " {0c}))) /\ ((dom g1) /\ ((dom g) \ (g " {0c}))) by Def1
.= ((dom f1) /\ ((dom f) /\ ((dom f) \ (f " {0c})))) /\ ((dom g1) /\ ((dom g) \ (g " {0c}))) by Th6
.= (((dom f) /\ ((dom f) \ (f " {0c}))) /\ (dom f1)) /\ (((dom g) /\ ((dom g) \ (g " {0c}))) /\ (dom g1)) by Th6
.= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((dom f1) /\ (((dom g) /\ ((dom g) \ (g " {0c}))) /\ (dom g1))) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ (((dom f1) /\ ((dom g) /\ ((dom g) \ (g " {0c})))) /\ (dom g1)) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((((dom f1) /\ (dom g)) /\ ((dom g) \ (g " {0c}))) /\ (dom g1)) by XBOOLE_1:16
.= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ (((dom (f1 (#) g)) /\ ((dom g) \ (g " {0c}))) /\ (dom g1)) by Th3
.= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((dom (f1 (#) g)) /\ ((dom g1) /\ ((dom g) \ (g " {0c})))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ ((((dom f) \ (f " {0c})) /\ (dom f)) /\ ((dom g1) /\ ((dom g) \ (g " {0c})))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ ((dom f) /\ ((dom g1) /\ ((dom g) \ (g " {0c}))))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ (((dom g1) /\ (dom f)) /\ ((dom g) \ (g " {0c})))) by XBOOLE_1:16
.= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ ((dom (g1 (#) f)) /\ ((dom g) \ (g " {0c})))) by Th3
.= (dom (f1 (#) g)) /\ ((dom (g1 (#) f)) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c})))) by XBOOLE_1:16
.= ((dom (f1 (#) g)) /\ (dom (g1 (#) f))) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c}))) by XBOOLE_1:16
.= (dom ((f1 (#) g) + (g1 (#) f))) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c}))) by VALUED_1:def_1
.= (dom ((f1 (#) g) + (g1 (#) f))) /\ ((dom (f (#) g)) \ ((f (#) g) " {0c})) by Th7
.= dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Def1 ;
hence  (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) by A1, PARTFUN2:1; ::_thesis: verum
end;

theorem :: CFUNCT_1:49
for C being non empty set
for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)
proof
let C be non empty set ; ::_thesis: for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)
let f, g, f1, g1 be PartFunc of C,COMPLEX; ::_thesis: (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1)
thus (f / g) / (f1 / g1) = (f / g) (#) ((f1 / g1) ^) by Th39
.= (f / g) (#) ((g1 | (dom (g1 ^))) / f1) by Th43
.= (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) by Th42 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:50
for C being non empty set
for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
proof
let C be non empty set ; ::_thesis: for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
let f1, f, g1, g be PartFunc of C,COMPLEX; ::_thesis: (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g)
thus (f1 / f) - (g1 / g) = (f1 / f) + (((- 1r) (#) g1) / g) by Th40, COMPLEX1:def_4
.= ((f1 (#) g) + (((- 1r) (#) g1) (#) f)) / (f (#) g) by Th48
.= ((f1 (#) g) - (g1 (#) f)) / (f (#) g) by Th17, COMPLEX1:def_4 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:51
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 / f2).| = |.f1.| / |.f2.|
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 / f2).| = |.f1.| / |.f2.|
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: |.(f1 / f2).| = |.f1.| / |.f2.|
thus |.(f1 / f2).| = |.(f1 (#) (f2 ^)).| by Th39
.= |.f1.| (#) |.(f2 ^).| by Th29
.= |.f1.| (#) (|.f2.| ^) by Th38
.= |.f1.| / |.f2.| by RFUNCT_1:31 ; ::_thesis: verum
end;

theorem Th52: :: CFUNCT_1:52
for X being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
proof
let X be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_(f2_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = ((f1 | X) + (f2 | X)) /. c )
assume A2: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = ((f1 | X) + (f2 | X)) /. c
then A3: c in (dom (f1 + f2)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
A5: c in dom (f1 + f2) by A3, XBOOLE_0:def_4;
then A6: c in (dom f1) /\ (dom f2) by VALUED_1:def_1;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A4, XBOOLE_0:def_4;
then A7: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A6, XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A4, XBOOLE_0:def_4;
then A8: c in dom (f1 | X) by RELAT_1:61;
then  c in (dom (f1 | X)) /\ (dom (f2 | X)) by A7, XBOOLE_0:def_4;
then A9: c in dom ((f1 | X) + (f2 | X)) by VALUED_1:def_1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A2, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A5, Th1
.= ((f1 | X) /. c) + (f2 /. c) by A8, PARTFUN2:15
.= ((f1 | X) /. c) + ((f2 | X) /. c) by A7, PARTFUN2:15
.= ((f1 | X) + (f2 | X)) /. c by A9, Th1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ (X /\ X) by VALUED_1:def_1
.= (dom f1) /\ ((dom f2) /\ (X /\ X)) by XBOOLE_1:16
.= (dom f1) /\ (((dom f2) /\ X) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (X /\ (dom (f2 | X))) by RELAT_1:61
.= ((dom f1) /\ X) /\ (dom (f2 | X)) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom (f2 | X)) by RELAT_1:61
.= dom ((f1 | X) + (f2 | X)) by VALUED_1:def_1 ;
hence  (f1 + f2) | X = (f1 | X) + (f2 | X) by A1, PARTFUN2:1; ::_thesis: ( (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) )
A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_f2)_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = ((f1 | X) + f2) /. c )
assume A11: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = ((f1 | X) + f2) /. c
then A12: c in (dom (f1 + f2)) /\ X by RELAT_1:61;
then A13: c in X by XBOOLE_0:def_4;
A14: c in dom (f1 + f2) by A12, XBOOLE_0:def_4;
then A15: c in (dom f1) /\ (dom f2) by VALUED_1:def_1;
then  c in dom f1 by XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A13, XBOOLE_0:def_4;
then A16: c in dom (f1 | X) by RELAT_1:61;
 c in dom f2 by A15, XBOOLE_0:def_4;
then  c in (dom (f1 | X)) /\ (dom f2) by A16, XBOOLE_0:def_4;
then A17: c in dom ((f1 | X) + f2) by VALUED_1:def_1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A11, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A14, Th1
.= ((f1 | X) /. c) + (f2 /. c) by A16, PARTFUN2:15
.= ((f1 | X) + f2) /. c by A17, Th1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_1
.= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61
.= dom ((f1 | X) + f2) by VALUED_1:def_1 ;
hence  (f1 + f2) | X = (f1 | X) + f2 by A10, PARTFUN2:1; ::_thesis: (f1 + f2) | X = f1 + (f2 | X)
A18: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_
((f1_+_f2)_|_X)_/._c_=_(f1_+_(f2_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) /. c = (f1 + (f2 | X)) /. c )
assume A19: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) /. c = (f1 + (f2 | X)) /. c
then A20: c in (dom (f1 + f2)) /\ X by RELAT_1:61;
then A21: c in X by XBOOLE_0:def_4;
A22: c in dom (f1 + f2) by A20, XBOOLE_0:def_4;
then A23: c in (dom f1) /\ (dom f2) by VALUED_1:def_1;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A21, XBOOLE_0:def_4;
then A24: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A23, XBOOLE_0:def_4;
then  c in (dom f1) /\ (dom (f2 | X)) by A24, XBOOLE_0:def_4;
then A25: c in dom (f1 + (f2 | X)) by VALUED_1:def_1;
thus ((f1 + f2) | X) /. c = (f1 + f2) /. c by A19, PARTFUN2:15
.= (f1 /. c) + (f2 /. c) by A22, Th1
.= (f1 /. c) + ((f2 | X) /. c) by A24, PARTFUN2:15
.= (f1 + (f2 | X)) /. c by A25, Th1 ; ::_thesis: verum
end;
dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_1
.= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61
.= dom (f1 + (f2 | X)) by VALUED_1:def_1 ;
hence  (f1 + f2) | X = f1 + (f2 | X) by A18, PARTFUN2:1; ::_thesis: verum
end;

theorem Th53: :: CFUNCT_1:53
for X being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
proof
let X be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_(f2_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. c )
assume A2: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = ((f1 | X) (#) (f2 | X)) /. c
then A3: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
A5: c in dom (f1 (#) f2) by A3, XBOOLE_0:def_4;
then A6: c in (dom f1) /\ (dom f2) by Th3;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A4, XBOOLE_0:def_4;
then A7: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A6, XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A4, XBOOLE_0:def_4;
then A8: c in dom (f1 | X) by RELAT_1:61;
then  c in (dom (f1 | X)) /\ (dom (f2 | X)) by A7, XBOOLE_0:def_4;
then A9: c in dom ((f1 | X) (#) (f2 | X)) by Th3;
thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A2, PARTFUN2:15
.= (f1 /. c) * (f2 /. c) by A5, Th3
.= ((f1 | X) /. c) * (f2 /. c) by A8, PARTFUN2:15
.= ((f1 | X) /. c) * ((f2 | X) /. c) by A7, PARTFUN2:15
.= ((f1 | X) (#) (f2 | X)) /. c by A9, Th3 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ (X /\ X) by Th3
.= (dom f1) /\ ((dom f2) /\ (X /\ X)) by XBOOLE_1:16
.= (dom f1) /\ (((dom f2) /\ X) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (X /\ (dom (f2 | X))) by RELAT_1:61
.= ((dom f1) /\ X) /\ (dom (f2 | X)) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom (f2 | X)) by RELAT_1:61
.= dom ((f1 | X) (#) (f2 | X)) by Th3 ;
hence  (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) by A1, PARTFUN2:1; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) )
A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_f2)_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c )
assume A11: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = ((f1 | X) (#) f2) /. c
then A12: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A13: c in X by XBOOLE_0:def_4;
A14: c in dom (f1 (#) f2) by A12, XBOOLE_0:def_4;
then A15: c in (dom f1) /\ (dom f2) by Th3;
then  c in dom f1 by XBOOLE_0:def_4;
then  c in (dom f1) /\ X by A13, XBOOLE_0:def_4;
then A16: c in dom (f1 | X) by RELAT_1:61;
 c in dom f2 by A15, XBOOLE_0:def_4;
then  c in (dom (f1 | X)) /\ (dom f2) by A16, XBOOLE_0:def_4;
then A17: c in dom ((f1 | X) (#) f2) by Th3;
thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A11, PARTFUN2:15
.= (f1 /. c) * (f2 /. c) by A14, Th3
.= ((f1 | X) /. c) * (f2 /. c) by A16, PARTFUN2:15
.= ((f1 | X) (#) f2) /. c by A17, Th3 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by Th3
.= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16
.= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61
.= dom ((f1 | X) (#) f2) by Th3 ;
hence  (f1 (#) f2) | X = (f1 | X) (#) f2 by A10, PARTFUN2:1; ::_thesis: (f1 (#) f2) | X = f1 (#) (f2 | X)
A18: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_
((f1_(#)_f2)_|_X)_/._c_=_(f1_(#)_(f2_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) /. c = (f1 (#) (f2 | X)) /. c )
assume A19: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) /. c = (f1 (#) (f2 | X)) /. c
then A20: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61;
then A21: c in X by XBOOLE_0:def_4;
A22: c in dom (f1 (#) f2) by A20, XBOOLE_0:def_4;
then A23: c in (dom f1) /\ (dom f2) by Th3;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in (dom f2) /\ X by A21, XBOOLE_0:def_4;
then A24: c in dom (f2 | X) by RELAT_1:61;
 c in dom f1 by A23, XBOOLE_0:def_4;
then  c in (dom f1) /\ (dom (f2 | X)) by A24, XBOOLE_0:def_4;
then A25: c in dom (f1 (#) (f2 | X)) by Th3;
thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A19, PARTFUN2:15
.= (f1 /. c) * (f2 /. c) by A22, Th3
.= (f1 /. c) * ((f2 | X) /. c) by A24, PARTFUN2:15
.= (f1 (#) (f2 | X)) /. c by A25, Th3 ; ::_thesis: verum
end;
dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61
.= ((dom f1) /\ (dom f2)) /\ X by Th3
.= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16
.= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61
.= dom (f1 (#) (f2 | X)) by Th3 ;
hence  (f1 (#) f2) | X = f1 (#) (f2 | X) by A18, PARTFUN2:1; ::_thesis: verum
end;

theorem Th54: :: CFUNCT_1:54
for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
proof
let X be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX holds
( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
let f be PartFunc of C,COMPLEX; ::_thesis: ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
A1: dom ((f ^) | X) = (dom (f ^)) /\ X by RELAT_1:61
.= ((dom f) \ (f " {0c})) /\ X by Def2
.= ((dom f) /\ X) \ ((f " {0c}) /\ X) by XBOOLE_1:50
.= (dom (f | X)) \ (X /\ (f " {0c})) by RELAT_1:61
.= (dom (f | X)) \ ((f | X) " {0c}) by FUNCT_1:70
.= dom ((f | X) ^) by Def2 ;
A2: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((-_f)_|_X)_holds_
((-_f)_|_X)_/._c_=_(-_(f_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((- f) | X) implies ((- f) | X) /. c = (- (f | X)) /. c )
assume A3: c in dom ((- f) | X) ; ::_thesis: ((- f) | X) /. c = (- (f | X)) /. c
then A4: c in (dom (- f)) /\ X by RELAT_1:61;
then A5: c in X by XBOOLE_0:def_4;
A6: c in dom (- f) by A4, XBOOLE_0:def_4;
then  c in dom f by Th5;
then  c in (dom f) /\ X by A5, XBOOLE_0:def_4;
then A7: c in dom (f | X) by RELAT_1:61;
then A8: c in dom (- (f | X)) by Th5;
thus ((- f) | X) /. c = (- f) /. c by A3, PARTFUN2:15
.= - (f /. c) by A6, Th5
.= - ((f | X) /. c) by A7, PARTFUN2:15
.= (- (f | X)) /. c by A8, Th5 ; ::_thesis: verum
end;
dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61
.= (dom f) /\ X by Th5
.= dom (f | X) by RELAT_1:61
.= dom (- (f | X)) by Th5 ;
hence  (- f) | X = - (f | X) by A2, PARTFUN2:1; ::_thesis: ( (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| )
A9: dom ((f | X) ^) c= dom (f | X) by Th6;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f_^)_|_X)_holds_
((f_^)_|_X)_/._c_=_((f_|_X)_^)_/._c
let c be Element of C; ::_thesis: ( c in dom ((f ^) | X) implies ((f ^) | X) /. c = ((f | X) ^) /. c )
assume A10: c in dom ((f ^) | X) ; ::_thesis: ((f ^) | X) /. c = ((f | X) ^) /. c
then  c in (dom (f ^)) /\ X by RELAT_1:61;
then A11: c in dom (f ^) by XBOOLE_0:def_4;
thus ((f ^) | X) /. c = (f ^) /. c by A10, PARTFUN2:15
.= (f /. c) " by A11, Def2
.= ((f | X) /. c) " by A9, A1, A10, PARTFUN2:15
.= ((f | X) ^) /. c by A1, A10, Def2 ; ::_thesis: verum
end;
hence  (f ^) | X = (f | X) ^ by A1, PARTFUN2:1; ::_thesis: |.f.| | X = |.(f | X).|
A12: dom (|.f.| | X) = (dom |.f.|) /\ X by RELAT_1:61
.= (dom f) /\ X by VALUED_1:def_11
.= dom (f | X) by RELAT_1:61
.= dom |.(f | X).| by VALUED_1:def_11 ;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(|.f.|_|_X)_holds_
(|.f.|_|_X)_._c_=_|.(f_|_X).|_._c
let c be Element of C; ::_thesis: ( c in dom (|.f.| | X) implies (|.f.| | X) . c = |.(f | X).| . c )
A13: dom |.f.| = dom f by VALUED_1:def_11;
assume A14: c in dom (|.f.| | X) ; ::_thesis: (|.f.| | X) . c = |.(f | X).| . c
then A15: c in dom (f | X) by A12, VALUED_1:def_11;
 c in (dom |.f.|) /\ X by A14, RELAT_1:61;
then A16: c in dom |.f.| by XBOOLE_0:def_4;
thus (|.f.| | X) . c = |.f.| . c by A14, FUNCT_1:47
.= |.(f . c).| by VALUED_1:18
.= |.(f /. c).| by A16, A13, PARTFUN1:def_6
.= |.((f | X) /. c).| by A15, PARTFUN2:15
.= |.((f | X) . c).| by A15, PARTFUN1:def_6
.= |.(f | X).| . c by VALUED_1:18 ; ::_thesis: verum
end;
hence  |.f.| | X = |.(f | X).| by A12, PARTFUN1:5; ::_thesis: verum
end;

theorem :: CFUNCT_1:55
for X being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
proof
let X be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
thus (f1 - f2) | X = (f1 | X) + ((- f2) | X) by Th52
.= (f1 | X) - (f2 | X) by Th54 ; ::_thesis: ( (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) )
thus (f1 - f2) | X = (f1 | X) + (- f2) by Th52
.= (f1 | X) - f2 ; ::_thesis: (f1 - f2) | X = f1 - (f2 | X)
thus (f1 - f2) | X = f1 + ((- f2) | X) by Th52
.= f1 - (f2 | X) by Th54 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:56
for X being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
proof
let X be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th39
.= (f1 | X) (#) ((f2 ^) | X) by Th53
.= (f1 | X) (#) ((f2 | X) ^) by Th54
.= (f1 | X) / (f2 | X) by Th39 ; ::_thesis: ( (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) )
thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th39
.= (f1 | X) (#) (f2 ^) by Th53
.= (f1 | X) / f2 by Th39 ; ::_thesis: (f1 / f2) | X = f1 / (f2 | X)
thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th39
.= f1 (#) ((f2 ^) | X) by Th53
.= f1 (#) ((f2 | X) ^) by Th54
.= f1 / (f2 | X) by Th39 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:57
for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X)
proof
let X be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X)
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X)
let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X)
let r be Element of COMPLEX ; ::_thesis: (r (#) f) | X = r (#) (f | X)
A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_(#)_f)_|_X)_holds_
((r_(#)_f)_|_X)_/._c_=_(r_(#)_(f_|_X))_/._c
let c be Element of C; ::_thesis: ( c in dom ((r (#) f) | X) implies ((r (#) f) | X) /. c = (r (#) (f | X)) /. c )
assume A2: c in dom ((r (#) f) | X) ; ::_thesis: ((r (#) f) | X) /. c = (r (#) (f | X)) /. c
then A3: c in (dom (r (#) f)) /\ X by RELAT_1:61;
then A4: c in X by XBOOLE_0:def_4;
A5: c in dom (r (#) f) by A3, XBOOLE_0:def_4;
then  c in dom f by Th4;
then  c in (dom f) /\ X by A4, XBOOLE_0:def_4;
then A6: c in dom (f | X) by RELAT_1:61;
then A7: c in dom (r (#) (f | X)) by Th4;
thus ((r (#) f) | X) /. c = (r (#) f) /. c by A2, PARTFUN2:15
.= r * (f /. c) by A5, Th4
.= r * ((f | X) /. c) by A6, PARTFUN2:15
.= (r (#) (f | X)) /. c by A7, Th4 ; ::_thesis: verum
end;
dom ((r (#) f) | X) = (dom (r (#) f)) /\ X by RELAT_1:61
.= (dom f) /\ X by Th4
.= dom (f | X) by RELAT_1:61
.= dom (r (#) (f | X)) by Th4 ;
hence  (r (#) f) | X = r (#) (f | X) by A1, PARTFUN2:1; ::_thesis: verum
end;

begin

theorem Th58: :: CFUNCT_1:58
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
thus  ( ( f1 is total & f2 is total ) iff f1 + f2 is total ) ::_thesis: ( ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) )
proof
thus  ( f1 is total & f2 is total implies f1 + f2 is total ) ::_thesis: ( f1 + f2 is total implies ( f1 is total & f2 is total ) )
proof
assume  ( f1 is total & f2 is total ) ; ::_thesis: f1 + f2 is total
then  ( dom f1 = C & dom f2 = C ) by PARTFUN1:def_2;
hence  dom (f1 + f2) = C /\ C by VALUED_1:def_1
.= C ;
:: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  f1 + f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 + f2) = C by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = C by VALUED_1:def_1;
then  ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
thus  ( ( f1 is total & f2 is total ) iff f1 - f2 is total ) ::_thesis: ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total )
proof
thus  ( f1 is total & f2 is total implies f1 - f2 is total ) ::_thesis: ( f1 - f2 is total implies ( f1 is total & f2 is total ) )
proof
assume  ( f1 is total & f2 is total ) ; ::_thesis: f1 - f2 is total
then  ( dom f1 = C & dom f2 = C ) by PARTFUN1:def_2;
hence  dom (f1 - f2) = C /\ C by Th2
.= C ;
:: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  f1 - f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 - f2) = C by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = C by Th2;
then  ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
thus  ( f1 is total & f2 is total implies f1 (#) f2 is total ) ::_thesis: ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) )
proof
assume  ( f1 is total & f2 is total ) ; ::_thesis: f1 (#) f2 is total
then  ( dom f1 = C & dom f2 = C ) by PARTFUN1:def_2;
hence  dom (f1 (#) f2) = C /\ C by Th3
.= C ;
:: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  f1 (#) f2 is total ; ::_thesis: ( f1 is total & f2 is total )
then  dom (f1 (#) f2) = C by PARTFUN1:def_2;
then  (dom f1) /\ (dom f2) = C by Th3;
then  ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17;
hence  ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem Th59: :: CFUNCT_1:59
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds
( f is total iff r (#) f is total )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds
( f is total iff r (#) f is total )
let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds
( f is total iff r (#) f is total )
let r be Element of COMPLEX ; ::_thesis: ( f is total iff r (#) f is total )
thus  ( f is total implies r (#) f is total ) ::_thesis: ( r (#) f is total implies f is total )
proof
assume  f is total ; ::_thesis: r (#) f is total
then  dom f = C by PARTFUN1:def_2;
hence  dom (r (#) f) = C by Th4; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  r (#) f is total ; ::_thesis: f is total
then  dom (r (#) f) = C by PARTFUN1:def_2;
hence  dom f = C by Th4; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem Th60: :: CFUNCT_1:60
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f is total iff - f is total )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( f is total iff - f is total )
let f be PartFunc of C,COMPLEX; ::_thesis: ( f is total iff - f is total )
A1: - f = (- 1r) (#) f by COMPLEX1:def_4;
thus  ( f is total implies - f is total ) ::_thesis: ( - f is total implies f is total )
proof
A2: - f = (- 1r) (#) f by COMPLEX1:def_4;
assume  f is total ; ::_thesis: - f is total
hence  - f is total by A2, Th59; ::_thesis: verum
end;
assume  - f is total ; ::_thesis: f is total
hence  f is total by A1, Th59; ::_thesis: verum
end;

theorem Th61: :: CFUNCT_1:61
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f is total iff |.f.| is total )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( f is total iff |.f.| is total )
let f be PartFunc of C,COMPLEX; ::_thesis: ( f is total iff |.f.| is total )
thus  ( f is total implies |.f.| is total ) ::_thesis: ( |.f.| is total implies f is total )
proof
assume  f is total ; ::_thesis: |.f.| is total
then  dom f = C by PARTFUN1:def_2;
hence  dom |.f.| = C by VALUED_1:def_11; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume  |.f.| is total ; ::_thesis: f is total
then  dom |.f.| = C by PARTFUN1:def_2;
hence  dom f = C by VALUED_1:def_11; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem Th62: :: CFUNCT_1:62
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f ^ is total iff ( f " {0} = {} & f is total ) )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( f ^ is total iff ( f " {0} = {} & f is total ) )
let f be PartFunc of C,COMPLEX; ::_thesis: ( f ^ is total iff ( f " {0} = {} & f is total ) )
thus  ( f ^ is total implies ( f " {0} = {} & f is total ) ) ::_thesis: ( f " {0} = {} & f is total implies f ^ is total )
proof
assume  f ^ is total ; ::_thesis: ( f " {0} = {} & f is total )
then A1: dom (f ^) = C by PARTFUN1:def_2;
 f " {0c} c= C ;
then  f " {0c} c= (dom f) \ (f " {0c}) by A1, Def2;
hence  f " {0} = {} by XBOOLE_1:38; ::_thesis: f is total
then  C = (dom f) \ {} by A1, Def2;
hence  dom f = C ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
assume A2: ( f " {0} = {} & f is total ) ; ::_thesis: f ^ is total
thus  dom (f ^) = (dom f) \ (f " {0c}) by Def2
.= C by A2, PARTFUN1:def_2 ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;

theorem Th63: :: CFUNCT_1:63
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX holds
( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )
proof
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )
thus  ( f1 is total & f2 " {0} = {} & f2 is total implies f1 / f2 is total ) ::_thesis: ( f1 / f2 is total implies ( f1 is total & f2 " {0} = {} & f2 is total ) )
proof
assume that
A1: f1 is total and
A2: ( f2 " {0} = {} & f2 is total ) ; ::_thesis: f1 / f2 is total
 f2 ^ is total by A2, Th62;
then  f1 (#) (f2 ^) is total by A1, Th58;
hence  f1 / f2 is total by Th39; ::_thesis: verum
end;
assume  f1 / f2 is total ; ::_thesis: ( f1 is total & f2 " {0} = {} & f2 is total )
then A3: f1 (#) (f2 ^) is total by Th39;
hence  f1 is total by Th58; ::_thesis: ( f2 " {0} = {} & f2 is total )
 f2 ^ is total by A3, Th58;
hence  ( f2 " {0} = {} & f2 is total ) by Th62; ::_thesis: verum
end;

theorem :: CFUNCT_1:64
for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C,COMPLEX st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) & (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) )
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f1, f2 being PartFunc of C,COMPLEX st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) & (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) )
let c be Element of C; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 is total & f2 is total holds
( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) & (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 is total & f2 is total implies ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) & (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) )
assume A1: ( f1 is total & f2 is total ) ; ::_thesis: ( (f1 + f2) /. c = (f1 /. c) + (f2 /. c) & (f1 - f2) /. c = (f1 /. c) - (f2 /. c) & (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) )
then  f1 + f2 is total by Th58;
then  dom (f1 + f2) = C by PARTFUN1:def_2;
hence  (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by Th1; ::_thesis: ( (f1 - f2) /. c = (f1 /. c) - (f2 /. c) & (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) )
 f1 - f2 is total by A1, Th58;
then  dom (f1 - f2) = C by PARTFUN1:def_2;
hence  (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by Th2; ::_thesis: (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c)
 f1 (#) f2 is total by A1, Th58;
then  dom (f1 (#) f2) = C by PARTFUN1:def_2;
hence  (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) by Th3; ::_thesis: verum
end;

theorem :: CFUNCT_1:65
for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f is total holds
(r (#) f) /. c = r * (f /. c)
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f is total holds
(r (#) f) /. c = r * (f /. c)
let c be Element of C; ::_thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f is total holds
(r (#) f) /. c = r * (f /. c)
let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX st f is total holds
(r (#) f) /. c = r * (f /. c)
let r be Element of COMPLEX ; ::_thesis: ( f is total implies (r (#) f) /. c = r * (f /. c) )
assume  f is total ; ::_thesis: (r (#) f) /. c = r * (f /. c)
then  r (#) f is total by Th59;
then  dom (r (#) f) = C by PARTFUN1:def_2;
hence  (r (#) f) /. c = r * (f /. c) by Th4; ::_thesis: verum
end;

theorem :: CFUNCT_1:66
for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX st f is total holds
( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,COMPLEX st f is total holds
( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )
let c be Element of C; ::_thesis: for f being PartFunc of C,COMPLEX st f is total holds
( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )
let f be PartFunc of C,COMPLEX; ::_thesis: ( f is total implies ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| ) )
assume A1: f is total ; ::_thesis: ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| )
then  |.f.| is total by Th61;
then A2: ( dom |.f.| = dom f & dom |.f.| = C ) by PARTFUN1:def_2, VALUED_1:def_11;
 - f is total by A1, Th60;
then  dom (- f) = C by PARTFUN1:def_2;
hence  (- f) /. c = - (f /. c) by Th5; ::_thesis: |.f.| . c = |.(f /. c).|
thus |.f.| . c = |.(f . c).| by VALUED_1:18
.= |.(f /. c).| by A2, PARTFUN1:def_6 ; ::_thesis: verum
end;

theorem :: CFUNCT_1:67
for C being non empty set
for c being Element of C
for f being PartFunc of C,COMPLEX st f ^ is total holds
(f ^) /. c = (f /. c) "
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f being PartFunc of C,COMPLEX st f ^ is total holds
(f ^) /. c = (f /. c) "
let c be Element of C; ::_thesis: for f being PartFunc of C,COMPLEX st f ^ is total holds
(f ^) /. c = (f /. c) "
let f be PartFunc of C,COMPLEX; ::_thesis: ( f ^ is total implies (f ^) /. c = (f /. c) " )
assume  f ^ is total ; ::_thesis: (f ^) /. c = (f /. c) "
then  dom (f ^) = C by PARTFUN1:def_2;
hence  (f ^) /. c = (f /. c) " by Def2; ::_thesis: verum
end;

theorem :: CFUNCT_1:68
for C being non empty set
for c being Element of C
for f1, f2 being PartFunc of C,COMPLEX st f1 is total & f2 ^ is total holds
(f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ")
proof
let C be non empty set ; ::_thesis: for c being Element of C
for f1, f2 being PartFunc of C,COMPLEX st f1 is total & f2 ^ is total holds
(f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ")
let c be Element of C; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 is total & f2 ^ is total holds
(f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ")
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 is total & f2 ^ is total implies (f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ") )
assume that
A1: f1 is total and
A2: f2 ^ is total ; ::_thesis: (f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ")
 ( f2 " {0c} = {} & f2 is total ) by A2, Th62;
then  f1 / f2 is total by A1, Th63;
then  dom (f1 / f2) = C by PARTFUN1:def_2;
hence  (f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ") by Def1; ::_thesis: verum
end;

begin

Lm3:  for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
proof
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
let f be PartFunc of C,COMPLEX; ::_thesis: ( |.f.| is bounded iff f is bounded )
A1: dom f = dom |.f.| by VALUED_1:def_11;
thus  ( |.f.| is bounded implies f is bounded ) ::_thesis: ( f is bounded implies |.f.| is bounded )
proof
assume  |.f.| is bounded ; ::_thesis: f is bounded
then consider r1 being real number  such that
A2: for y being set st y in dom |.f.| holds
abs (|.f.| . y) < r1 by COMSEQ_2:def_3;
take  r1 ; :: according to COMSEQ_2:def_3 ::_thesis: for b1 being set holds
( not b1 in K104(f) or not r1 <= abs (f . b1) )
let y be set ; ::_thesis: ( not y in K104(f) or not r1 <= abs (f . y) )
assume A3: y in dom f ; ::_thesis: not r1 <= abs (f . y)
then  abs (|.f.| . y) < r1 by A1, A2;
then  abs |.(f . y).| < r1 by A1, A3, VALUED_1:def_11;
hence  not r1 <= abs (f . y) ; ::_thesis: verum
end;
given r1 being real number  such that A4: for y being set st y in dom f holds
abs (f . y) < r1 ; :: according to COMSEQ_2:def_3 ::_thesis: |.f.| is bounded
now__::_thesis:_ex_r1_being_real_number_st_
for_y_being_set_st_y_in_dom_|.f.|_holds_
abs_(|.f.|_._y)_<_r1
take r1 = r1; ::_thesis: for y being set st y in dom |.f.| holds
abs (|.f.| . y) < r1
let y be set ; ::_thesis: ( y in dom |.f.| implies abs (|.f.| . y) < r1 )
assume A5: y in dom |.f.| ; ::_thesis: abs (|.f.| . y) < r1
then  abs |.(f . y).| < r1 by A1, A4;
hence  abs (|.f.| . y) < r1 by A5, VALUED_1:def_11; ::_thesis: verum
end;
hence  |.f.| is bounded by COMSEQ_2:def_3; ::_thesis: verum
end;

theorem Th69: :: CFUNCT_1:69
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f | Y is bounded iff ex p being real number st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX holds
( f | Y is bounded iff ex p being real number st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds
( f | Y is bounded iff ex p being real number st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )
let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is bounded iff ex p being real number st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p )
A1: dom |.f.| = dom f by VALUED_1:def_11;
A2: dom (|.f.| | Y) = Y /\ (dom |.f.|) by RELAT_1:61;
A3: |.f.| | Y = |.(f | Y).| by RFUNCT_1:46;
hereby  ::_thesis: ( ex p being real number st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p implies f | Y is bounded )
assume  f | Y is bounded ; ::_thesis: ex p being real number st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p
then  |.f.| | Y is bounded by A3, Lm3;
then consider p being real number  such that
A4: for c being set st c in dom (|.f.| | Y) holds
abs ((|.f.| | Y) . c) <= p by RFUNCT_1:72;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_f)_holds_
|.(f_/._c).|_<=_p
let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies |.(f /. c).| <= p )
assume A5: c in Y /\ (dom f) ; ::_thesis: |.(f /. c).| <= p
 c in dom f by A5, XBOOLE_0:def_4;
then A6: f . c = f /. c by PARTFUN1:def_6;
abs ((|.f.| | Y) . c) = abs (|.f.| . c) by A1, A2, A5, FUNCT_1:47
.= abs |.(f . c).| by VALUED_1:18 ;
hence  |.(f /. c).| <= p by A1, A2, A4, A5, A6; ::_thesis: verum
end;
hence  ex p being real number st
for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p ; ::_thesis: verum
end;
given p being real number  such that A7: for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p ; ::_thesis: f | Y is bounded
A8: dom |.f.| = dom f by VALUED_1:def_11;
now__::_thesis:_for_c_being_set_st_c_in_dom_(|.f.|_|_Y)_holds_
abs_((|.f.|_|_Y)_._c)_<=_p
let c be set ; ::_thesis: ( c in dom (|.f.| | Y) implies abs ((|.f.| | Y) . c) <= p )
assume A9: c in dom (|.f.| | Y) ; ::_thesis: abs ((|.f.| | Y) . c) <= p
A10: c in dom |.f.| by A9, RELAT_1:57;
abs ((|.f.| | Y) . c) = abs (|.f.| . c) by A9, FUNCT_1:47
.= abs |.(f . c).| by VALUED_1:18
.= abs |.(f /. c).| by A1, A10, PARTFUN1:def_6 ;
hence  abs ((|.f.| | Y) . c) <= p by A2, A7, A8, A9; ::_thesis: verum
end;
then  |.f.| | Y is bounded by RFUNCT_1:72;
hence  f | Y is bounded by A3, Lm3; ::_thesis: verum
end;

theorem :: CFUNCT_1:70
for Y, X being set
for C being non empty set
for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds
f | Y is bounded
proof
let Y, X be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds
f | Y is bounded
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds
f | Y is bounded
let f be PartFunc of C,COMPLEX; ::_thesis: ( Y c= X & f | X is bounded implies f | Y is bounded )
assume that
A1: Y c= X and
A2: f | X is bounded ; ::_thesis: f | Y is bounded
 |.f.| | X = |.(f | X).| by RFUNCT_1:46;
then  |.f.| | X is bounded by A2, Lm3;
then  ( |.f.| | Y = |.(f | Y).| & |.f.| | Y is bounded ) by A1, RFUNCT_1:46, RFUNCT_1:74;
hence  f | Y is bounded by Lm3; ::_thesis: verum
end;

theorem :: CFUNCT_1:71
for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX st X misses dom f holds
f | X is bounded
proof
let X be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st X misses dom f holds
f | X is bounded
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st X misses dom f holds
f | X is bounded
let f be PartFunc of C,COMPLEX; ::_thesis: ( X misses dom f implies f | X is bounded )
assume  X /\ (dom f) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f | X is bounded
then  for c being Element of C st c in X /\ (dom f) holds
|.(f /. c).| <= 0 ;
hence  f | X is bounded by Th69; ::_thesis: verum
end;

theorem Th72: :: CFUNCT_1:72
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f | Y is bounded holds
(r (#) f) | Y is bounded
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f | Y is bounded holds
(r (#) f) | Y is bounded
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st f | Y is bounded holds
(r (#) f) | Y is bounded
let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX st f | Y is bounded holds
(r (#) f) | Y is bounded
let r be Element of COMPLEX ; ::_thesis: ( f | Y is bounded implies (r (#) f) | Y is bounded )
assume A1: f | Y is bounded ; ::_thesis: (r (#) f) | Y is bounded
 |.f.| | Y = |.(f | Y).| by RFUNCT_1:46;
then  |.f.| | Y is bounded by A1, Lm3;
then  (|.r.| (#) |.f.|) | Y is bounded by RFUNCT_1:80;
then  ( |.(r (#) f).| | Y = |.((r (#) f) | Y).| & |.(r (#) f).| | Y is bounded ) by Th30, RFUNCT_1:46;
hence  (r (#) f) | Y is bounded by Lm3; ::_thesis: verum
end;

theorem :: CFUNCT_1:73
for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below
proof
let X be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below
let f be PartFunc of C,COMPLEX; ::_thesis: |.f.| | X is bounded_below
now__::_thesis:_ex_z_being_Element_of_NAT_st_
for_c_being_set_st_c_in_X_/\_(dom_|.f.|)_holds_
z_<=_|.f.|_._c
take z = 0 ; ::_thesis: for c being set st c in X /\ (dom |.f.|) holds
z <= |.f.| . c
let c be set ; ::_thesis: ( c in X /\ (dom |.f.|) implies z <= |.f.| . c )
A1: z <= |.(f /. c).| by COMPLEX1:46;
assume  c in X /\ (dom |.f.|) ; ::_thesis: z <= |.f.| . c
then A2: c in dom |.f.| by XBOOLE_0:def_4;
 dom |.f.| = dom f by VALUED_1:def_11;
then  f . c = f /. c by A2, PARTFUN1:def_6;
hence  z <= |.f.| . c by A1, VALUED_1:18; ::_thesis: verum
end;
hence  |.f.| | X is bounded_below by RFUNCT_1:71; ::_thesis: verum
end;

theorem Th74: :: CFUNCT_1:74
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is bounded holds
( |.f.| | Y is bounded & (- f) | Y is bounded )
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is bounded holds
( |.f.| | Y is bounded & (- f) | Y is bounded )
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | Y is bounded holds
( |.f.| | Y is bounded & (- f) | Y is bounded )
let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is bounded implies ( |.f.| | Y is bounded & (- f) | Y is bounded ) )
assume A1: f | Y is bounded ; ::_thesis: ( |.f.| | Y is bounded & (- f) | Y is bounded )
 |.f.| | Y = |.(f | Y).| by RFUNCT_1:46;
hence  |.f.| | Y is bounded by A1, Lm3; ::_thesis: (- f) | Y is bounded
 (- 1r) (#) (f | Y) = ((- 1r) (#) f) | Y by RFUNCT_1:49;
hence  (- f) | Y is bounded by A1, Th72, COMPLEX1:def_4; ::_thesis: verum
end;

theorem Th75: :: CFUNCT_1:75
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
(f1 + f2) | (X /\ Y) is bounded
proof
let X, Y be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
(f1 + f2) | (X /\ Y) is bounded
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
(f1 + f2) | (X /\ Y) is bounded
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded )
assume that
A1: f1 | X is bounded and
A2: f2 | Y is bounded ; ::_thesis: (f1 + f2) | (X /\ Y) is bounded
consider r1 being real number  such that
A3: for c being Element of C st c in X /\ (dom f1) holds
|.(f1 /. c).| <= r1 by A1, Th69;
consider r2 being real number  such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
|.(f2 /. c).| <= r2 by A2, Th69;
 ex p1 being real number st
for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds
|.((f1 + f2) /. c).| <= p1
proof
take r0 = r1 + r2; ::_thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds
|.((f1 + f2) /. c).| <= r0
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies |.((f1 + f2) /. c).| <= r0 )
A5: |.((f1 /. c) + (f2 /. c)).| <= |.(f1 /. c).| + |.(f2 /. c).| by COMPLEX1:56;
assume A6: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: |.((f1 + f2) /. c).| <= r0
then A7: c in X /\ Y by XBOOLE_0:def_4;
then A8: c in X by XBOOLE_0:def_4;
A9: c in Y by A7, XBOOLE_0:def_4;
A10: c in dom (f1 + f2) by A6, XBOOLE_0:def_4;
then A11: c in (dom f1) /\ (dom f2) by VALUED_1:def_1;
then  c in dom f2 by XBOOLE_0:def_4;
then  c in Y /\ (dom f2) by A9, XBOOLE_0:def_4;
then A12: |.(f2 /. c).| <= r2 by A4;
 c in dom f1 by A11, XBOOLE_0:def_4;
then  c in X /\ (dom f1) by A8, XBOOLE_0:def_4;
then  |.(f1 /. c).| <= r1 by A3;
then  |.(f1 /. c).| + |.(f2 /. c).| <= r0 by A12, XREAL_1:7;
then  |.((f1 /. c) + (f2 /. c)).| <= r0 by A5, XXREAL_0:2;
hence  |.((f1 + f2) /. c).| <= r0 by A10, Th1; ::_thesis: verum
end;
hence  (f1 + f2) | (X /\ Y) is bounded by Th69; ::_thesis: verum
end;

theorem Th76: :: CFUNCT_1:76
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
proof
let X, Y be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 | X is bounded & f2 | Y is bounded implies ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) )
assume that
A1: f1 | X is bounded and
A2: f2 | Y is bounded ; ::_thesis: ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
consider r1 being real number  such that
A3: for c being Element of C st c in X /\ (dom f1) holds
|.(f1 /. c).| <= r1 by A1, Th69;
consider r2 being real number  such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
|.(f2 /. c).| <= r2 by A2, Th69;
now__::_thesis:_ex_r_being_set_st_
for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_
|.((f1_(#)_f2)_/._c).|_<=_r
take r = r1 * r2; ::_thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds
|.((f1 (#) f2) /. c).| <= r
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies |.((f1 (#) f2) /. c).| <= r )
assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: |.((f1 (#) f2) /. c).| <= r
then A6: c in X /\ Y by XBOOLE_0:def_4;
then A7: c in X by XBOOLE_0:def_4;
A8: c in dom (f1 (#) f2) by A5, XBOOLE_0:def_4;
then A9: c in (dom f1) /\ (dom f2) by Th3;
then  c in dom f1 by XBOOLE_0:def_4;
then  c in X /\ (dom f1) by A7, XBOOLE_0:def_4;
then A10: |.(f1 /. c).| <= r1 by A3;
A11: c in Y by A6, XBOOLE_0:def_4;
 c in dom f2 by A9, XBOOLE_0:def_4;
then  c in Y /\ (dom f2) by A11, XBOOLE_0:def_4;
then A12: |.(f2 /. c).| <= r2 by A4;
 ( 0 <= |.(f1 /. c).| & 0 <= |.(f2 /. c).| ) by COMPLEX1:46;
then  |.(f1 /. c).| * |.(f2 /. c).| <= r by A10, A12, XREAL_1:66;
then  |.((f1 /. c) * (f2 /. c)).| <= r by COMPLEX1:65;
hence  |.((f1 (#) f2) /. c).| <= r by A8, Th3; ::_thesis: verum
end;
hence  (f1 (#) f2) | (X /\ Y) is bounded by Th69; ::_thesis: (f1 - f2) | (X /\ Y) is bounded
 (- f2) | Y is bounded by A2, Th74;
hence  (f1 - f2) | (X /\ Y) is bounded by A1, Th75; ::_thesis: verum
end;

theorem :: CFUNCT_1:77
for X, Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
proof
let X, Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
let f be PartFunc of C,COMPLEX; ::_thesis: ( f | X is bounded & f | Y is bounded implies f | (X \/ Y) is bounded )
assume that
A1: f | X is bounded and
A2: f | Y is bounded ; ::_thesis: f | (X \/ Y) is bounded
 |.f.| | Y = |.(f | Y).| by RFUNCT_1:46;
then A3: |.f.| | Y is bounded by A2, Lm3;
 |.f.| | X = |.(f | X).| by RFUNCT_1:46;
then  |.f.| | X is bounded by A1, Lm3;
then  ( |.f.| | (X \/ Y) = |.(f | (X \/ Y)).| & |.f.| | (X \/ Y) is bounded ) by A3, RFUNCT_1:46, RFUNCT_1:87;
hence  f | (X \/ Y) is bounded by Lm3; ::_thesis: verum
end;

theorem :: CFUNCT_1:78
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
proof
let X, Y be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 | X is constant & f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 | X is constant & f2 | Y is constant implies ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) )
assume that
A1: f1 | X is constant and
A2: f2 | Y is constant ; ::_thesis: ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
consider cr1 being Element of COMPLEX  such that
A3: for c being Element of C st c in X /\ (dom f1) holds
f1 /. c = cr1 by A1, PARTFUN2:35;
consider cr2 being Element of COMPLEX  such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
f2 /. c = cr2 by A2, PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_+_f2))_holds_
(f1_+_f2)_/._c_=_cr1_+_cr2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) /. c = cr1 + cr2 )
assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: (f1 + f2) /. c = cr1 + cr2
then A6: c in X /\ Y by XBOOLE_0:def_4;
then A7: c in X by XBOOLE_0:def_4;
A8: c in dom (f1 + f2) by A5, XBOOLE_0:def_4;
then A9: c in (dom f1) /\ (dom f2) by VALUED_1:def_1;
then  c in dom f1 by XBOOLE_0:def_4;
then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def_4;
A11: c in Y by A6, XBOOLE_0:def_4;
 c in dom f2 by A9, XBOOLE_0:def_4;
then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def_4;
thus (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by A8, Th1
.= cr1 + (f2 /. c) by A3, A10
.= cr1 + cr2 by A4, A12 ; ::_thesis: verum
end;
hence  (f1 + f2) | (X /\ Y) is constant by PARTFUN2:35; ::_thesis: ( (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant )
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_-_f2))_holds_
(f1_-_f2)_/._c_=_cr1_-_cr2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) /. c = cr1 - cr2 )
assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; ::_thesis: (f1 - f2) /. c = cr1 - cr2
then A14: c in X /\ Y by XBOOLE_0:def_4;
then A15: c in X by XBOOLE_0:def_4;
A16: c in dom (f1 - f2) by A13, XBOOLE_0:def_4;
then A17: c in (dom f1) /\ (dom f2) by Th2;
then  c in dom f1 by XBOOLE_0:def_4;
then A18: c in X /\ (dom f1) by A15, XBOOLE_0:def_4;
A19: c in Y by A14, XBOOLE_0:def_4;
 c in dom f2 by A17, XBOOLE_0:def_4;
then A20: c in Y /\ (dom f2) by A19, XBOOLE_0:def_4;
thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A16, Th2
.= cr1 - (f2 /. c) by A3, A18
.= cr1 - cr2 by A4, A20 ; ::_thesis: verum
end;
hence  (f1 - f2) | (X /\ Y) is constant by PARTFUN2:35; ::_thesis: (f1 (#) f2) | (X /\ Y) is constant
now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_
(f1_(#)_f2)_/._c_=_cr1_*_cr2
let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = cr1 * cr2 )
assume A21: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: (f1 (#) f2) /. c = cr1 * cr2
then A22: c in X /\ Y by XBOOLE_0:def_4;
then A23: c in X by XBOOLE_0:def_4;
A24: c in dom (f1 (#) f2) by A21, XBOOLE_0:def_4;
then A25: c in (dom f1) /\ (dom f2) by Th3;
then  c in dom f1 by XBOOLE_0:def_4;
then A26: c in X /\ (dom f1) by A23, XBOOLE_0:def_4;
A27: c in Y by A22, XBOOLE_0:def_4;
 c in dom f2 by A25, XBOOLE_0:def_4;
then A28: c in Y /\ (dom f2) by A27, XBOOLE_0:def_4;
thus (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) by A24, Th3
.= cr1 * (f2 /. c) by A3, A26
.= cr1 * cr2 by A4, A28 ; ::_thesis: verum
end;
hence  (f1 (#) f2) | (X /\ Y) is constant by PARTFUN2:35; ::_thesis: verum
end;

theorem Th79: :: CFUNCT_1:79
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX
for q being Element of COMPLEX st f | Y is constant holds
(q (#) f) | Y is constant
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX
for q being Element of COMPLEX st f | Y is constant holds
(q (#) f) | Y is constant
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX
for q being Element of COMPLEX st f | Y is constant holds
(q (#) f) | Y is constant
let f be PartFunc of C,COMPLEX; ::_thesis: for q being Element of COMPLEX st f | Y is constant holds
(q (#) f) | Y is constant
let q be Element of COMPLEX ; ::_thesis: ( f | Y is constant implies (q (#) f) | Y is constant )
assume  f | Y is constant ; ::_thesis: (q (#) f) | Y is constant
then consider r being Element of COMPLEX  such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(q_(#)_f))_holds_
(q_(#)_f)_/._c_=_q_*_r
let c be Element of C; ::_thesis: ( c in Y /\ (dom (q (#) f)) implies (q (#) f) /. c = q * r )
assume A2: c in Y /\ (dom (q (#) f)) ; ::_thesis: (q (#) f) /. c = q * r
then A3: c in Y by XBOOLE_0:def_4;
A4: c in dom (q (#) f) by A2, XBOOLE_0:def_4;
then  c in dom f by Th4;
then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def_4;
thus (q (#) f) /. c = q * (f /. c) by A4, Th4
.= q * r by A1, A5 ; ::_thesis: verum
end;
hence  (q (#) f) | Y is constant by PARTFUN2:35; ::_thesis: verum
end;

theorem Th80: :: CFUNCT_1:80
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
( |.f.| | Y is constant & (- f) | Y is constant )
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
( |.f.| | Y is constant & (- f) | Y is constant )
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | Y is constant holds
( |.f.| | Y is constant & (- f) | Y is constant )
let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is constant implies ( |.f.| | Y is constant & (- f) | Y is constant ) )
assume  f | Y is constant ; ::_thesis: ( |.f.| | Y is constant & (- f) | Y is constant )
then consider r being Element of COMPLEX  such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_|.f.|)_holds_
|.f.|_._c_=_|.r.|
let c be Element of C; ::_thesis: ( c in Y /\ (dom |.f.|) implies |.f.| . c = |.r.| )
assume A2: c in Y /\ (dom |.f.|) ; ::_thesis: |.f.| . c = |.r.|
then  c in dom |.f.| by XBOOLE_0:def_4;
then A3: c in dom f by VALUED_1:def_11;
 c in Y by A2, XBOOLE_0:def_4;
then A4: c in Y /\ (dom f) by A3, XBOOLE_0:def_4;
 f . c = f /. c by A3, PARTFUN1:def_6;
hence |.f.| . c = |.(f /. c).| by VALUED_1:18
.= |.r.| by A1, A4 ;
::_thesis: verum
end;
hence  |.f.| | Y is constant by PARTFUN2:57; ::_thesis: (- f) | Y is constant
now__::_thesis:_ex_p_being_Element_of_COMPLEX_st_
for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(-_f))_holds_
(-_f)_/._c_=_p
take p = - r; ::_thesis: for c being Element of C st c in Y /\ (dom (- f)) holds
(- f) /. c = p
let c be Element of C; ::_thesis: ( c in Y /\ (dom (- f)) implies (- f) /. c = p )
assume A5: c in Y /\ (dom (- f)) ; ::_thesis: (- f) /. c = p
then  c in Y /\ (dom f) by Th5;
then A6: - (f /. c) = p by A1;
 c in dom (- f) by A5, XBOOLE_0:def_4;
hence  (- f) /. c = p by A6, Th5; ::_thesis: verum
end;
hence  (- f) | Y is constant by PARTFUN2:35; ::_thesis: verum
end;

theorem Th81: :: CFUNCT_1:81
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
f | Y is bounded
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
f | Y is bounded
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | Y is constant holds
f | Y is bounded
let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is constant implies f | Y is bounded )
assume  f | Y is constant ; ::_thesis: f | Y is bounded
then consider r being Element of COMPLEX  such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
now__::_thesis:_ex_p_being_Element_of_REAL_st_
for_c_being_Element_of_C_st_c_in_Y_/\_(dom_f)_holds_
|.(f_/._c).|_<=_p
take p = |.r.|; ::_thesis: for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p
let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies |.(f /. c).| <= p )
assume  c in Y /\ (dom f) ; ::_thesis: |.(f /. c).| <= p
hence  |.(f /. c).| <= p by A1; ::_thesis: verum
end;
hence  f | Y is bounded by Th69; ::_thesis: verum
end;

theorem :: CFUNCT_1:82
for Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )
proof
let Y be set ; ::_thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )
let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | Y is constant holds
( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )
let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is constant implies ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded ) )
assume A1: f | Y is constant ; ::_thesis: ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )
hence  for r being Element of COMPLEX holds (r (#) f) | Y is bounded by Th79, Th81; ::_thesis: ( (- f) | Y is bounded & |.f.| | Y is bounded )
thus  (- f) | Y is bounded by A1, Th80, Th81; ::_thesis: |.f.| | Y is bounded
 |.f.| | Y is constant by A1, Th80;
hence  |.f.| | Y is bounded ; ::_thesis: verum
end;

theorem Th83: :: CFUNCT_1:83
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds
(f1 + f2) | (X /\ Y) is bounded
proof
let X, Y be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds
(f1 + f2) | (X /\ Y) is bounded
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds
(f1 + f2) | (X /\ Y) is bounded
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 | X is bounded & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded )
assume that
A1: f1 | X is bounded and
A2: f2 | Y is constant ; ::_thesis: (f1 + f2) | (X /\ Y) is bounded
 f2 | Y is bounded by A2, Th81;
hence  (f1 + f2) | (X /\ Y) is bounded by A1, Th75; ::_thesis: verum
end;

theorem :: CFUNCT_1:84
for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds
( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )
proof
let X, Y be set ; ::_thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds
( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )
let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds
( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )
let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) )
assume that
A1: f1 | X is bounded and
A2: f2 | Y is constant ; ::_thesis: ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )
 (- f2) | Y is constant by A2, Th80;
hence  (f1 - f2) | (X /\ Y) is bounded by A1, Th83; ::_thesis: ( (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded )
A3: f2 | Y is bounded by A2, Th81;
hence  (f2 - f1) | (X /\ Y) is bounded by A1, Th76; ::_thesis: (f1 (#) f2) | (X /\ Y) is bounded
thus  (f1 (#) f2) | (X /\ Y) is bounded by A1, A3, Th76; ::_thesis: verum
end;

theorem :: CFUNCT_1:85
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded ) by Lm3;