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, Th61;
then f1 (#) (f2 ^) is total by A1, Th57;
hence f1 / f2 is total by Th38; :: thesis: verum
end;
assume f1 / f2 is total ; :: thesis: ( f1 is total & f2 " {0} = {} & f2 is total )
then A3: f1 (#) (f2 ^) is total by Th38;
hence f1 is total by Th57; :: thesis: ( f2 " {0} = {} & f2 is total )
f2 ^ is total by A3, Th57;
hence ( f2 " {0} = {} & f2 is total ) by Th61; :: thesis: verum