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 ) )
proof
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;
assume f1 / f2 is total ; :: thesis: ( 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