let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X, Y being set
for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & 0 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))
let F be PartFunc of D,REAL; :: thesis: for X, Y being set
for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & 0 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))
let X, Y be set ; :: thesis: for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & 0 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))
let Z be finite set ; :: thesis: ( Z = dom (F | Y) & dom (F | X) is finite & Y c= X & 0 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) implies FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y))) )
assume A1: Z = dom (F | Y) ; :: thesis: ( not dom (F | X) is finite or not Y c= X or not 0 = card Z or ex d1, d2 being Element of D st
( d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) & not F . d1 >= F . d2 ) or FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y))) )
assume that
A2: dom (F | X) is finite and
Y c= X and
A3: 0 = card Z and
for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ; :: thesis: FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))
A4: dom (F | Y) = {} by A1, A3;
A5: dom (F | (X \ Y)) = (dom F) /\ (X \ Y) by RELAT_1:61;
( dom (F | X) = (dom F) /\ X & dom (F | Y) = (dom F) /\ Y ) by RELAT_1:61;
then dom (F | (X \ Y)) = (dom (F | X)) \ {} by A5, A4, XBOOLE_1:50
.= dom (F | X) ;
then A6: FinS (F,(X \ Y)) = FinS (F,(dom (F | X))) by A2, Th63
.= FinS (F,X) by A2, Th63 ;
FinS (F,Y) = FinS (F,{}) by A4, Th63
.= {} by Th68 ;
hence FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y))) by A6, FINSEQ_1:34; :: thesis: verum