let D be non empty set ; :: thesis: for d being Element of D
for X being set
for F being PartFunc of D,REAL st dom (F | X) is finite & d in dom (F | X) holds
(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent
let d be Element of D; :: thesis: for X being set
for F being PartFunc of D,REAL st dom (F | X) is finite & d in dom (F | X) holds
(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent
let X be set ; :: thesis: for F being PartFunc of D,REAL st dom (F | X) is finite & d in dom (F | X) holds
(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent
let F be PartFunc of D,REAL; :: thesis: ( dom (F | X) is finite & d in dom (F | X) implies (FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent )
set dx = dom (F | X);
assume that
A1: dom (F | X) is finite and
A2: d in dom (F | X) ; :: thesis: (FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent
set Y = X \ {d};
set dy = dom (F | (X \ {d}));
A3: dom (F | (X \ {d})) = (dom F) /\ (X \ {d}) by RELAT_1:61;
A4: dom (F | X) = (dom F) /\ X by RELAT_1:61;
A5: dom (F | (X \ {d})) = (dom (F | X)) \ {d}
proof
thus dom (F | (X \ {d})) c= (dom (F | X)) \ {d} :: according to XBOOLE_0:def 10 :: thesis: (dom (F | X)) \ {d} c= dom (F | (X \ {d}))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (F | (X \ {d})) or y in (dom (F | X)) \ {d} )
assume A6: y in dom (F | (X \ {d})) ; :: thesis: y in (dom (F | X)) \ {d}
then y in X \ {d} by A3, XBOOLE_0:def 4;
then A7: not y in {d} by XBOOLE_0:def 5;
y in dom F by A3, A6, XBOOLE_0:def 4;
then y in dom (F | X) by A3, A4, A6, XBOOLE_0:def 4;
hence y in (dom (F | X)) \ {d} by A7, XBOOLE_0:def 5; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (dom (F | X)) \ {d} or y in dom (F | (X \ {d})) )
assume A8: y in (dom (F | X)) \ {d} ; :: thesis: y in dom (F | (X \ {d}))
then A9: not y in {d} by XBOOLE_0:def 5;
A10: y in dom (F | X) by A8, XBOOLE_0:def 5;
then y in X by A4, XBOOLE_0:def 4;
then A11: y in X \ {d} by A9, XBOOLE_0:def 5;
y in dom F by A4, A10, XBOOLE_0:def 4;
hence y in dom (F | (X \ {d})) by A3, A11, XBOOLE_0:def 4; :: thesis: verum
end;
F | (dom (F | X)) = F | ((dom F) /\ X) by RELAT_1:61
.= (F | (dom F)) | X by RELAT_1:71
.= F | X by RELAT_1:68 ;
then (FinS (F,((dom (F | X)) \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent by A1, A2, Th65;
hence (FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent by A1, A5, Th63; :: thesis: verum