A1: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(Lm3, Lm4);
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, 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 that
A2: dom (F | X) is finite and
A3: Y c= X and
A4: 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))
F | Y c= F | X by A3, 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, A3, A4; :: thesis: verum