A1: for n being Nat holds S₁[n] from NAT_1:sch 2(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: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; :: thesis: verum