let m, n be non zero Element of NAT ; :: thesis: ( m <= n implies ex A being FinSequence of n -tuples_on BOOLEAN st

( len A = m & A is one-to-one & card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) ) )

assume A1: m <= n ; :: thesis: ex A being FinSequence of n -tuples_on BOOLEAN st

( len A = m & A is one-to-one & card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) )

defpred S_{1}[ Nat, Function] means for j being Nat st j in Seg n holds

( ( $1 = j implies $2 . j = TRUE ) & ( $1 <> j implies $2 . j = FALSE ) );

A2: for k being Nat st k in Seg m holds

ex x being Element of n -tuples_on BOOLEAN st S_{1}[k,x]

A7: ( dom A = Seg m & ( for k being Nat st k in Seg m holds

S_{1}[k,A . k] ) )
from FINSEQ_1:sch 5(A2);

take A ; :: thesis: ( len A = m & A is one-to-one & card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) )

thus len A = m by A7, FINSEQ_1:def 3; :: thesis: ( A is one-to-one & card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) )

A8: for x, y being object st x in dom A & y in dom A & A . x = A . y holds

x = y

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) )

A12: card (dom A) = m by FINSEQ_1:57, A7;

dom A, rng A are_equipotent by A8, FUNCT_1:def 4, WELLORD2:def 4;

hence card (rng A) = m by A12, CARD_1:5; :: thesis: for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) )

thus for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) by A7; :: thesis: verum

( len A = m & A is one-to-one & card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) ) )

assume A1: m <= n ; :: thesis: ex A being FinSequence of n -tuples_on BOOLEAN st

( len A = m & A is one-to-one & card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) )

defpred S

( ( $1 = j implies $2 . j = TRUE ) & ( $1 <> j implies $2 . j = FALSE ) );

A2: for k being Nat st k in Seg m holds

ex x being Element of n -tuples_on BOOLEAN st S

proof

consider A being FinSequence of n -tuples_on BOOLEAN such that
let k be Nat; :: thesis: ( k in Seg m implies ex x being Element of n -tuples_on BOOLEAN st S_{1}[k,x] )

assume k in Seg m ; :: thesis: ex x being Element of n -tuples_on BOOLEAN st S_{1}[k,x]

defpred S_{2}[ Nat, set ] means ( ( k = $1 implies $2 = TRUE ) & ( k <> $1 implies $2 = FALSE ) );

A3: for j being Nat st j in Seg n holds

ex y being Element of BOOLEAN st S_{2}[j,y]

A6: ( dom x = Seg n & ( for j being Nat st j in Seg n holds

S_{2}[j,x . j] ) )
from FINSEQ_1:sch 5(A3);

reconsider x = x as Element of BOOLEAN * by FINSEQ_1:def 11;

len x = n by A6, FINSEQ_1:def 3;

then x in { s where s is Element of BOOLEAN * : len s = n } ;

then reconsider x = x as Element of n -tuples_on BOOLEAN ;

take x ; :: thesis: S_{1}[k,x]

thus S_{1}[k,x]
by A6; :: thesis: verum

end;assume k in Seg m ; :: thesis: ex x being Element of n -tuples_on BOOLEAN st S

defpred S

A3: for j being Nat st j in Seg n holds

ex y being Element of BOOLEAN st S

proof

consider x being FinSequence of BOOLEAN such that
let j be Nat; :: thesis: ( j in Seg n implies ex y being Element of BOOLEAN st S_{2}[j,y] )

assume j in Seg n ; :: thesis: ex y being Element of BOOLEAN st S_{2}[j,y]

end;assume j in Seg n ; :: thesis: ex y being Element of BOOLEAN st S

A6: ( dom x = Seg n & ( for j being Nat st j in Seg n holds

S

reconsider x = x as Element of BOOLEAN * by FINSEQ_1:def 11;

len x = n by A6, FINSEQ_1:def 3;

then x in { s where s is Element of BOOLEAN * : len s = n } ;

then reconsider x = x as Element of n -tuples_on BOOLEAN ;

take x ; :: thesis: S

thus S

A7: ( dom A = Seg m & ( for k being Nat st k in Seg m holds

S

take A ; :: thesis: ( len A = m & A is one-to-one & card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) )

thus len A = m by A7, FINSEQ_1:def 3; :: thesis: ( A is one-to-one & card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) )

A8: for x, y being object st x in dom A & y in dom A & A . x = A . y holds

x = y

proof

hence
A is one-to-one
by FUNCT_1:def 4; :: thesis: ( card (rng A) = m & ( for i, j being Nat st i in Seg m & j in Seg n holds
let x, y be object ; :: thesis: ( x in dom A & y in dom A & A . x = A . y implies x = y )

assume A9: ( x in dom A & y in dom A & A . x = A . y ) ; :: thesis: x = y

then reconsider i1 = x, i2 = y as Nat ;

assume A10: x <> y ; :: thesis: contradiction

A11: Seg m c= Seg n by A1, FINSEQ_1:5;

(A . i2) . i1 = FALSE by A10, A9, A7, A11;

hence contradiction by A9, A7, A11; :: thesis: verum

end;assume A9: ( x in dom A & y in dom A & A . x = A . y ) ; :: thesis: x = y

then reconsider i1 = x, i2 = y as Nat ;

assume A10: x <> y ; :: thesis: contradiction

A11: Seg m c= Seg n by A1, FINSEQ_1:5;

(A . i2) . i1 = FALSE by A10, A9, A7, A11;

hence contradiction by A9, A7, A11; :: thesis: verum

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) )

A12: card (dom A) = m by FINSEQ_1:57, A7;

dom A, rng A are_equipotent by A8, FUNCT_1:def 4, WELLORD2:def 4;

hence card (rng A) = m by A12, CARD_1:5; :: thesis: for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) )

thus for i, j being Nat st i in Seg m & j in Seg n holds

( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) by A7; :: thesis: verum