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: dom ((f / g) (#) (f1 / g1)) = (dom (f / g)) /\ (dom (f1 / g1)) by Th5
.= ((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 Th5
.= (dom (f (#) f1)) /\ ((dom (g (#) g1)) \ ((g (#) g1) " {0c })) by Th16
.= dom ((f (#) f1) / (g (#) g1)) by Def1 ;

now

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 Th5;
then c in (dom (f (#) (g ^ ))) /\ (dom (f1 / g1)) by Th51;
then c in (dom (f (#) (g ^ ))) /\ (dom (f1 (#) (g1 ^ ))) by Th51;
then A3: ( c in dom (f (#) (g ^ )) & c in dom (f1 (#) (g1 ^ )) ) by XBOOLE_0:def 4;
then ( c in (dom f) /\ (dom (g ^ )) & c in (dom f1) /\ (dom (g1 ^ )) ) by Th5;
then ( c in dom f & c in dom (g ^ ) & c in dom f1 & c in dom (g1 ^ ) ) by XBOOLE_0:def 4;
then ( c in (dom f) /\ (dom f1) & c in (dom (g ^ )) /\ (dom (g1 ^ )) ) by XBOOLE_0:def 4;
then A4: ( c in dom (f (#) f1) & c in dom ((g ^ ) (#) (g1 ^ )) ) by Th5;
then ( c in dom (f (#) f1) & c in dom ((g (#) g1) ^ ) ) by Th45;
then c in (dom (f (#) f1)) /\ (dom ((g (#) g1) ^ )) by XBOOLE_0:def 4;
then A5: c in dom ((f (#) f1) (#) ((g (#) g1) ^ )) by Th5;
thus ((f / g) (#) (f1 / g1)) /. c = ((f / g) /. c) * ((f1 / g1) /. c) by A2, Th5
.= ((f (#) (g ^ )) /. c) * ((f1 / g1) /. c) by Th51
.= ((f (#) (g ^ )) /. c) * ((f1 (#) (g1 ^ )) /. c) by Th51
.= ((f /. c) * ((g ^ ) /. c)) * ((f1 (#) (g1 ^ )) /. c) by A3, Th5
.= ((f /. c) * ((g ^ ) /. c)) * ((f1 /. c) * ((g1 ^ ) /. c)) by A3, Th5
.= (f /. c) * ((f1 /. c) * (((g ^ ) /. c) * ((g1 ^ ) /. c)))
.= (f /. c) * ((f1 /. c) * (((g ^ ) (#) (g1 ^ )) /. c)) by A4, Th5
.= ((f /. c) * (f1 /. c)) * (((g ^ ) (#) (g1 ^ )) /. c)
.= ((f /. c) * (f1 /. c)) * (((g (#) g1) ^ ) /. c) by Th45
.= ((f (#) f1) /. c) * (((g (#) g1) ^ ) /. c) by A4, Th5
.= ((f (#) f1) (#) ((g (#) g1) ^ )) /. c by A5, Th5
.= ((f (#) f1) / (g (#) g1)) /. c by Th51 ; :: thesis: verum

end;

hence (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) by A1, PARTFUN2:3; :: thesis: verum