A1:
for n being Nat holds S1[n]
from NAT_1:sch 2(Lm3, Lm4);
let D be non empty set ; 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; 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 ; ( 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
; FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))
F | Y c= F | X
by A3, RELAT_1:75;
then reconsider dFY = dom (F | Y) as finite set by A2, FINSET_1:1, RELAT_1:11;
card dFY = card dFY
;
hence
FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y)))
by A1, A2, A3, A4; verum