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