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 S1[ 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 S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg m implies ex x being Element of n -tuples_on BOOLEAN st S1[k,x] )
assume k in Seg m ; :: thesis: ex x being Element of n -tuples_on BOOLEAN st S1[k,x]
defpred S2[ 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 S2[j,y]
proof
let j be Nat; :: thesis: ( j in Seg n implies ex y being Element of BOOLEAN st S2[j,y] )
assume j in Seg n ; :: thesis: ex y being Element of BOOLEAN st S2[j,y]
per cases ( k = j or k <> j ) ;
suppose A4: k = j ; :: thesis: ex y being Element of BOOLEAN st S2[j,y]
take TRUE ; :: thesis: S2[j, TRUE ]
thus S2[j, TRUE ] by A4; :: thesis: verum
end;
suppose A5: k <> j ; :: thesis: ex y being Element of BOOLEAN st S2[j,y]
take FALSE ; :: thesis: S2[j, FALSE ]
thus S2[j, FALSE ] by A5; :: thesis: verum
end;
end;
end;
consider x being FinSequence of BOOLEAN such that
A6: ( dom x = Seg n & ( for j being Nat st j in Seg n holds
S2[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: S1[k,x]
thus S1[k,x] by A6; :: thesis: verum
end;
consider A being FinSequence of n -tuples_on BOOLEAN such that
A7: ( dom A = Seg m & ( for k being Nat st k in Seg m holds
S1[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
proof
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;
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
( ( 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