let X, Y be set ; :: thesis: for n being natural number st X c= Y holds
free_magma X,n c= free_magma Y,n
let n be natural number ; :: thesis: ( X c= Y implies free_magma X,n c= free_magma Y,n )
defpred S₁[ Nat] means ( X c= Y implies free_magma X,$1 c= free_magma Y,$1 );
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A2: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
thus ( X c= Y implies free_magma X,k c= free_magma Y,k ) :: thesis: verum

proof

assume A3: X c= Y ; :: thesis: free_magma X,k c= free_magma Y,k
( k = 0 or k + 1 > 0 + 1 ) by XREAL_1:8;
then ( k = 0 or k >= 1 ) by NAT_1:13;
then ( k = 0 or k = 1 or k > 1 ) by XXREAL_0:1;
then A4: ( k = 0 or k = 1 or k + 1 > 1 + 1 ) by XREAL_1:8;

per cases ( k = 0 or k = 1 or k >= 2 ) by A4, NAT_1:13;

suppose k = 0 ; :: thesis: free_magma X,k c= free_magma Y,k

then ( free_magma X,k = {} & free_magma Y,k = {} ) by Def14;
hence free_magma X,k c= free_magma Y,k ; :: thesis: verum

end;

suppose k = 1 ; :: thesis: free_magma X,k c= free_magma Y,k

then ( free_magma X,k = X & free_magma Y,k = Y ) by Def14;
hence free_magma X,k c= free_magma Y,k by A3; :: thesis: verum

end;

suppose A5: k >= 2 ; :: thesis: free_magma X,k c= free_magma Y,k

for x being set st x in free_magma X,k holds
x in free_magma Y,k

proof

let x be set ; :: thesis: ( x in free_magma X,k implies x in free_magma Y,k )
assume x in free_magma X,k ; :: thesis: x in free_magma Y,k
then consider p, m being natural number such that
A6: ( x `2 = p & 1 <= p & p <= k - 1 & (x `1 ) `1 in free_magma X,p & (x `1 ) `2 in free_magma X,m & k = p + m & x in [:[:(free_magma X,p),(free_magma X,m):],{p}:] ) by A5, Th21;
consider fs being FinSequence such that
A7: ( len fs = k - 1 & ( for p being natural number st p >= 1 & p <= k - 1 holds
fs . p = [:(free_magma Y,p),(free_magma Y,(k -' p)):] ) & free_magma Y,k = Union (disjoin fs) ) by A5, Th20;
A8: fs . p = [:(free_magma Y,p),(free_magma Y,(k -' p)):] by A6, A7;
A9: ( x `1 in [:(free_magma X,p),(free_magma X,m):] & x `2 in {p} ) by A6, MCART_1:10;
A10: x = [(x `1 ),(x `2 )] by A6, MCART_1:23;
A11: x `1 = [((x `1 ) `1 ),((x `1 ) `2 )] by A9, MCART_1:23;
p + 1 <= (k - 1) + 1 by A6, XREAL_1:9;
then A12: p < k by NAT_1:13;
then A13: free_magma X,p c= free_magma Y,p by A2, A3;
p - p < k - p by A12, XREAL_1:16;
then A14: k -' p = m by A6, XREAL_0:def 2;
p + m > 0 + m by A6, XREAL_1:10;
then free_magma X,m c= free_magma Y,(k -' p) by A6, A2, A3, A14;
then x `1 in [:(free_magma Y,p),(free_magma Y,(k -' p)):] by A6, A11, A13, MCART_1:11;
then A15: x in [:(fs . p),{p}:] by A8, A10, A9, MCART_1:11;
p in Seg (len fs) by A6, A7, FINSEQ_1:3;
then A16: p in dom fs by FINSEQ_1:def 3;
then A17: (disjoin fs) . p = [:(fs . p),{p}:] by CARD_3:def 3;
p in dom (disjoin fs) by A16, CARD_3:def 3;
then [:(fs . p),{p}:] in rng (disjoin fs) by A17, FUNCT_1:12;
then x in union (rng (disjoin fs)) by A15, TARSKI:def 4;
hence x in free_magma Y,k by A7, CARD_3:def 4; :: thesis: verum

end;

hence free_magma X,k c= free_magma Y,k by TARSKI:def 3; :: thesis: verum

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A1);
hence ( X c= Y implies free_magma X,n c= free_magma Y,n ) ; :: thesis: verum