let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,REAL holds

( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )

let f1, f2 be PartFunc of C,REAL; :: 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 ) )

then A4: f1 (#) (f2 ^) is total by Th31;

hence f1 is total by Th50; :: thesis: ( f2 " {0} = {} & f2 is total )

f2 ^ is total by A4, Th50;

hence ( f2 " {0} = {} & f2 is total ) by Th54; :: thesis: verum

( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total )

let f1, f2 be PartFunc of C,REAL; :: 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
f1 / f2 is total
; :: thesis: ( f1 is total & f2 " {0} = {} & f2 is total )
assume that

A1: f1 is total and

A2: f2 " {0} = {} and

A3: f2 is total ; :: thesis: f1 / f2 is total

f2 ^ is total by A2, A3, Th54;

then f1 (#) (f2 ^) is total by A1;

hence f1 / f2 is total by Th31; :: thesis: verum

end;A1: f1 is total and

A2: f2 " {0} = {} and

A3: f2 is total ; :: thesis: f1 / f2 is total

f2 ^ is total by A2, A3, Th54;

then f1 (#) (f2 ^) is total by A1;

hence f1 / f2 is total by Th31; :: thesis: verum

then A4: f1 (#) (f2 ^) is total by Th31;

hence f1 is total by Th50; :: thesis: ( f2 " {0} = {} & f2 is total )

f2 ^ is total by A4, Th50;

hence ( f2 " {0} = {} & f2 is total ) by Th54; :: thesis: verum