defpred S₁[ Element of 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: 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 A2: ( X1 c= X2 & X2 c= NAT & not {} in X2 & card X2 = 0 ) ; :: thesis: Product (Sgm X1) <= Product (Sgm X2)
then X2 = {} ;
hence Product (Sgm X1) <= Product (Sgm X2) by A2, XBOOLE_1:3; :: thesis: verum

end;

A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]

now

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 A5: ( X1 c= X2 & X2 c= NAT & not {} in X2 & 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 A5;
set m = max A;
set X11 = X1 \ {(max A)};
set X12 = X2 \ {(max A)};
A6: X1 \ {(max A)} c= X2 \ {(max A)} by A5, XBOOLE_1:33;
A7: X2 \ {(max A)} c= X2 by XBOOLE_1:36;
then A8: X2 \ {(max A)} c= NAT by A5, XBOOLE_1:1;
A9: max A in X2 by XXREAL_2:def 8;
then A10: (X2 \ {(max A)}) \/ {(max A)} = X2 by ZFMISC_1:140;
A11: (X2 \ {(max A)}) /\ {(max A)} = (X2 /\ {(max A)}) \ {(max A)} by XBOOLE_1:49
.= {(max A)} \ {(max A)} by A9, ZFMISC_1:52
.= {} 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:64;
then A12: card X2 = ((card (X2 \ {(max A)})) + 1) - (card {} ) by A10, A11, CARD_1:50;
A13: not {} in X2 \ {(max A)} by A5, A7;
then A14: Product (Sgm (X1 \ {(max A)})) <= Product (Sgm (X2 \ {(max A)})) by A4, A5, A8, A12, XBOOLE_1:33;
reconsider m = max A as Element of NAT by A5, A9;

now

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

end;

then A18: X2 \ {(max A)} c= Seg m by TARSKI:def 3;
A19: not m = 0 by A5, XXREAL_2:def 8;
then 0 + 1 < m + 1 by XREAL_1:8;
then A20: 1 <= m by NAT_1:13;
then m in Seg m by FINSEQ_1:3;
then A21: {m} c= Seg m by ZFMISC_1:37;

now

let n1, n2 be Element of NAT ; :: thesis: ( n1 in X2 \ {(max A)} & n2 in {m} implies n1 < n2 )
assume A22: ( n1 in X2 \ {(max A)} & n2 in {m} ) ; :: thesis: n1 < n2
then A23: n2 = m by TARSKI:def 1;
not n1 in {m} by A22, XBOOLE_0:def 5;
then A24: n1 <> m by TARSKI:def 1;
n1 <= m by A7, A22, XXREAL_2:def 8;
hence n1 < n2 by A23, A24, XXREAL_0:1; :: thesis: verum

end;

then Product (Sgm X2) = Product ((Sgm (X2 \ {(max A)})) ^ (Sgm {m})) by A10, A18, A21, FINSEQ_3:48;
then A25: Product (Sgm X2) = (Product (Sgm (X2 \ {(max A)}))) * (Product (Sgm {m})) by RVSUM_1:127
.= (Product (Sgm (X2 \ {(max A)}))) * (Product <*m*>) by A19, FINSEQ_3:50
.= (Product (Sgm (X2 \ {(max A)}))) * m by RVSUM_1:125 ;
A26: 1 * (Product (Sgm (X2 \ {(max A)}))) <= m * (Product (Sgm (X2 \ {(max A)}))) by A20, XREAL_1:66;

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

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

then A27: X1 = (X1 \ {(max A)}) \/ {m} by ZFMISC_1:140;

now

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

end;

then A31: X1 \ {(max A)} c= Seg m by TARSKI:def 3;

now

let n1, n2 be Element of NAT ; :: thesis: ( n1 in X1 \ {(max A)} & n2 in {m} implies n1 < n2 )
assume A32: ( n1 in X1 \ {(max A)} & n2 in {m} ) ; :: thesis: n1 < n2
then A33: n2 = m by TARSKI:def 1;
not n1 in {m} by A32, XBOOLE_0:def 5;
then A34: n1 <> m by TARSKI:def 1;
n1 in X2 \ {(max A)} by A6, A32;
then n1 <= m by A7, XXREAL_2:def 8;
hence n1 < n2 by A33, A34, XXREAL_0:1; :: thesis: verum

end;

then Product (Sgm X1) = Product ((Sgm (X1 \ {(max A)})) ^ (Sgm {m})) by A21, A27, A31, FINSEQ_3:48
.= (Product (Sgm (X1 \ {(max A)}))) * (Product (Sgm {m})) by RVSUM_1:127
.= (Product (Sgm (X1 \ {(max A)}))) * (Product <*m*>) by A19, FINSEQ_3:50
.= (Product (Sgm (X1 \ {(max A)}))) * m by RVSUM_1:125 ;
hence Product (Sgm X1) <= Product (Sgm X2) by A4, A5, A6, A8, A12, A13, A25, XREAL_1:66; :: 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:65;
hence Product (Sgm X1) <= Product (Sgm X2) by A25, A26, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

A35: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A3);
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)
let X2 be finite set ; :: thesis: ( X1 c= X2 & X2 c= NAT & not {} in X2 implies Product (Sgm X1) <= Product (Sgm X2) )
assume A36: ( X1 c= X2 & X2 c= NAT & not {} in X2 ) ; :: thesis: Product (Sgm X1) <= Product (Sgm X2)
ex n being Element of NAT st card X2 = n ;
hence Product (Sgm X1) <= Product (Sgm X2) by A35, A36; :: thesis: verum