let C, D be non empty set ; :: thesis: for SC being Subset of C
for d being Element of D st SC --> d is total holds
SC <> {}
let SC be Subset of C; :: thesis: for d being Element of D st SC --> d is total holds
SC <> {}
let d be Element of D; :: thesis: ( SC --> d is total implies SC <> {} )
assume that
A1: SC --> d is total and
A2: SC = {} ; :: thesis: contradiction
dom (SC --> d) = C by A1, PARTFUN1:def 2;
hence contradiction by A2, FUNCOP_1:10; :: thesis: verum