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 A2: ( 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 ) ) ; :: thesis: FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y))
A3: ( dom (F | X) = (dom F) /\ X & dom (F | Y) = (dom F) /\ Y & dom (F | (X \ Y)) = (dom F) /\ (X \ Y) ) by RELAT_1:90;
A4: dom (F | Y) = {} by A1, A2;
then A5: FinS F,Y = FinS F,{} by Th66
.= {} by Th71 ;
dom (F | (X \ Y)) = (dom (F | X)) \ {} by A3, A4, XBOOLE_1:50
.= dom (F | X) ;
then FinS F,(X \ Y) = FinS F,(dom (F | X)) by A2, Th66
.= FinS F,X by A2, Th66 ;
hence FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y)) by A5, FINSEQ_1:47; :: thesis: verum