let X1 be set ; :: thesis: for X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 holds
Product (Sgm X1) <= Product (Sgm X2)
defpred S₁[ Nat] means for X1 being set
for X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 & card X2 = $1 holds
Product (Sgm X1) <= Product (Sgm X2);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for X1 being set
for X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 & card X2 = n + 1 holds
Product (Sgm X1) <= Product (Sgm X2)

let X1 be set ; :: thesis: for X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 & card X2 = n + 1 holds
Product (Sgm b₂) <= Product (Sgm b₃)
let X2 be finite set ; :: thesis: ( X1 c= X2 & X2 c= NAT & not {} in X2 & card X2 = n + 1 implies Product (Sgm b₁) <= Product (Sgm b₂) )
assume that
A3: X1 c= X2 and
A4: X2 c= NAT and
A5: not {} in X2 and
A6: card X2 = n + 1 ; :: thesis: Product (Sgm b₁) <= Product (Sgm b₂)
set A = X2;
reconsider A = X2 as non empty finite real-membered set by A4, A6;
set m = max A;
set X11 = X1 \ {(max A)};
set X12 = X2 \ {(max A)};
A7: max A in X2 by XXREAL_2:def 8;
then A8: (X2 \ {(max A)}) \/ {(max A)} = X2 by ZFMISC_1:116;
A9: (X2 \ {(max A)}) /\ {(max A)} = (X2 /\ {(max A)}) \ {(max A)} by XBOOLE_1:49
.= {(max A)} \ {(max A)} by A7, ZFMISC_1:46
.= {} by XBOOLE_1:37 ;
card ((X2 \ {(max A)}) \/ {(max A)}) = ((card (X2 \ {(max A)})) + (card {(max A)})) - (card ((X2 \ {(max A)}) /\ {(max A)})) by CARD_2:45;
then A10: card X2 = ((card (X2 \ {(max A)})) + 1) - (card {}) by A8, A9, CARD_1:30;
reconsider m = max A as Element of NAT by A4, A7;
A11: X1 \ {(max A)} c= X2 \ {(max A)} by A3, XBOOLE_1:33;
A12: X2 \ {(max A)} c= X2 by XBOOLE_1:36;
then A13: ( X2 \ {(max A)} c= NAT & not {} in X2 \ {(max A)} ) by A4, A5;
then A14: Product (Sgm (X1 \ {(max A)})) <= Product (Sgm (X2 \ {(max A)})) by A2, A3, A6, A10, XBOOLE_1:33;

now :: thesis: for x being object st x in X2 \ {(max A)} holds
x in Seg m

let x be object ; :: thesis: ( x in X2 \ {(max A)} implies x in Seg m )
set r = x;
assume A15: x in X2 \ {(max A)} ; :: thesis: x in Seg m
then x in A by A12;
then reconsider r = x as Element of NAT by A4;
not r = 0 by A5, A12, A15;
then 0 + 1 < r + 1 by XREAL_1:6;
then A16: 1 <= r by NAT_1:13;
r <= m by A12, A15, XXREAL_2:def 8;
hence x in Seg m by A16, FINSEQ_1:1; :: thesis: verum

end;

then X2 \ {(max A)} c= Seg m ;
then a17: X2 \ {(max A)} is included_in_Seg by FINSEQ_1:def 13;
A18: not m = 0 by A5, XXREAL_2:def 8;
then 0 + 1 < m + 1 by XREAL_1:6;
then A19: 1 <= m by NAT_1:13;
then m in Seg m by FINSEQ_1:1;
then {m} c= Seg m by ZFMISC_1:31;
then a20: {m} is included_in_Seg by FINSEQ_1:def 13;

now :: thesis: for n1, n2 being Nat st n1 in X2 \ {(max A)} & n2 in {m} holds
n1 < n2

let n1, n2 be Nat; :: thesis: ( n1 in X2 \ {(max A)} & n2 in {m} implies n1 < n2 )
assume that
A21: n1 in X2 \ {(max A)} and
A22: n2 in {m} ; :: thesis: n1 < n2
not n1 in {m} by A21, XBOOLE_0:def 5;
then A23: n1 <> m by TARSKI:def 1;
( n2 = m & n1 <= m ) by A12, A21, A22, TARSKI:def 1, XXREAL_2:def 8;
hence n1 < n2 by A23, XXREAL_0:1; :: thesis: verum

end;

then Product (Sgm X2) = Product ((Sgm (X2 \ {(max A)})) ^ (Sgm {m})) by A8, a17, a20, FINSEQ_3:42;
then A24: Product (Sgm X2) = (Product (Sgm (X2 \ {(max A)}))) * (Product (Sgm {m})) by RVSUM_1:97
.= (Product (Sgm (X2 \ {(max A)}))) * (Product <*m*>) by A18, FINSEQ_3:44
.= (Product (Sgm (X2 \ {(max A)}))) * m ;
A25: 1 * (Product (Sgm (X2 \ {(max A)}))) <= m * (Product (Sgm (X2 \ {(max A)}))) by A19, XREAL_1:64;

per cases ( m in X1 or not m in X1 ) ;

suppose A26: m in X1 ; :: thesis: Product (Sgm b₁) <= Product (Sgm b₂)

A27: now :: thesis: for n1, n2 being Nat st n1 in X1 \ {(max A)} & n2 in {m} holds
n1 < n2

let n1, n2 be Nat; :: thesis: ( n1 in X1 \ {(max A)} & n2 in {m} implies n1 < n2 )
assume that
A28: n1 in X1 \ {(max A)} and
A29: n2 in {m} ; :: thesis: n1 < n2
not n1 in {m} by A28, XBOOLE_0:def 5;
then A30: n1 <> m by TARSKI:def 1;
n1 in X2 \ {(max A)} by A11, A28;
then A31: n1 <= m by A12, XXREAL_2:def 8;
n2 = m by A29, TARSKI:def 1;
hence n1 < n2 by A30, A31, XXREAL_0:1; :: thesis: verum

end;

now :: thesis: for x being object st x in X1 \ {(max A)} holds
x in Seg m

let x be object ; :: thesis: ( x in X1 \ {(max A)} implies x in Seg m )
set r = x;
assume x in X1 \ {(max A)} ; :: thesis: x in Seg m
then A32: x in X1 by XBOOLE_0:def 5;
then x in A by A3;
then reconsider r = x as Element of NAT by A4;
not r = 0 by A3, A5, A32;
then 0 + 1 < r + 1 by XREAL_1:6;
then A33: 1 <= r by NAT_1:13;
r <= m by A3, A32, XXREAL_2:def 8;
hence x in Seg m by A33, FINSEQ_1:1; :: thesis: verum

end;

then X1 \ {(max A)} c= Seg m ;
then a34: X1 \ {(max A)} is included_in_Seg by FINSEQ_1:def 13;
X1 = (X1 \ {(max A)}) \/ {m} by A26, ZFMISC_1:116;
then Product (Sgm X1) = Product ((Sgm (X1 \ {(max A)})) ^ (Sgm {m})) by a20, a34, A27, FINSEQ_3:42
.= (Product (Sgm (X1 \ {(max A)}))) * (Product (Sgm {m})) by RVSUM_1:97
.= (Product (Sgm (X1 \ {(max A)}))) * (Product <*m*>) by A18, FINSEQ_3:44
.= (Product (Sgm (X1 \ {(max A)}))) * m ;
hence Product (Sgm X1) <= Product (Sgm X2) by A2, A6, A11, A10, A13, A24, XREAL_1:64; :: thesis: verum

end;

suppose not m in X1 ; :: thesis: Product (Sgm b₁) <= Product (Sgm b₂)

then Product (Sgm X1) <= Product (Sgm (X2 \ {(max A)})) by A14, ZFMISC_1:57;
hence Product (Sgm X1) <= Product (Sgm X2) by A24, A25, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

let X2 be finite set ; :: thesis: ( X1 c= X2 & X2 c= NAT & not {} in X2 implies Product (Sgm X1) <= Product (Sgm X2) )
assume A35: ( X1 c= X2 & X2 c= NAT & not {} in X2 ) ; :: thesis: Product (Sgm X1) <= Product (Sgm X2)
A36: ex n being Element of NAT st card X2 = n ;
A37: S₁[ 0 ]

proof

let X1 be set ; :: thesis: for X2 being finite set st X1 c= X2 & X2 c= NAT & not {} in X2 & card X2 = 0 holds
Product (Sgm X1) <= Product (Sgm X2)
let X2 be finite set ; :: thesis: ( X1 c= X2 & X2 c= NAT & not {} in X2 & card X2 = 0 implies Product (Sgm X1) <= Product (Sgm X2) )
assume that
A38: X1 c= X2 and
X2 c= NAT and
not {} in X2 and
A39: card X2 = 0 ; :: thesis: Product (Sgm X1) <= Product (Sgm X2)
X2 = {} by A39;
hence Product (Sgm X1) <= Product (Sgm X2) by A38, XBOOLE_1:3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A37, A1);
hence Product (Sgm X1) <= Product (Sgm X2) by A35, A36; :: thesis: verum