let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X, Y being set st dom (F | X) is finite & Y c= X & ( 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 st dom (F | X) is finite & Y c= X & ( 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 be set ; :: thesis: for Y being set st dom (F | X) is finite & Y c= X & ( 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))
A1: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(Lm3, Lm4);
let Y be set ; :: thesis: ( dom (F | X) is finite & Y c= X & ( 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 A2: ( dom (F | X) is finite & Y c= X & ( 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))
then F | Y c= F | X by RELAT_1:104;
then reconsider dFY = dom (F | Y) as finite set by A2, FINSET_1:13, RELAT_1:25;
card dFY = card dFY ;
hence FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y)) by A1, A2; :: thesis: verum