let C, D be non empty set ; :: thesis: for SC being Subset of C
for d being Element of D holds
( SC --> d is total iff SC = C )
let SC be Subset of C; :: thesis: for d being Element of D holds
( SC --> d is total iff SC = C )
let d be Element of D; :: thesis: ( SC --> d is total iff SC = C )
thus ( SC --> d is total implies SC = C ) :: thesis: ( SC = C implies SC --> d is total )

proof

assume SC --> d is total ; :: thesis: SC = C
then dom (SC --> d) = C by PARTFUN1:def 2;
hence SC = C by FUNCOP_1:13; :: thesis: verum

end;

assume SC = C ; :: thesis: SC --> d is total
then dom (SC --> d) = C by FUNCOP_1:13;
hence SC --> d is total by PARTFUN1:def 2; :: thesis: verum