let X, Y be set ; :: thesis: for n being Nat st X c= Y holds
free_magma (X,n) c= free_magma (Y,n)
let n be Nat; :: 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:6;
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:6;

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 Def13;
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 Def13;
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 object st x in free_magma (X,k) holds
x in free_magma (Y,k)

proof

let x be object ; :: 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 Nat 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 Nat 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:21;
A11: x `1 = [((x `1) `1),((x `1) `2)] by A9, MCART_1:21;
p + 1 <= (k - 1) + 1 by A6, XREAL_1:7;
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:14;
then A14: k -' p = m by A6, XREAL_0:def 2;
p + m > 0 + m by A6, XREAL_1:8;
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, ZFMISC_1:def 2;
then A15: x in [:(fs . p),{p}:] by A8, A10, A9, ZFMISC_1:def 2;
p in Seg (len fs) by A6, A7, FINSEQ_1:1;
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:3;
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) ; :: 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