defpred S₁[ Nat] means for x1, x2, y1, y2 being FinSequence st len x1 = $1 & F₁() = x1 ^ x2 & len y1 = $1 & F₂() = y1 ^ y2 holds
P₁[y1 ^ x2];
A5: S₁[ 0 ]

proof

let x1, x2, y1, y2 be FinSequence; :: thesis: ( len x1 = 0 & F₁() = x1 ^ x2 & len y1 = 0 & F₂() = y1 ^ y2 implies P₁[y1 ^ x2] )
assume that
A6: len x1 = 0 and
A7: F₁() = x1 ^ x2 and
A8: len y1 = 0 and
F₂() = y1 ^ y2 ; :: thesis: P₁[y1 ^ x2]
A9: x1 = {} by A6;
y1 = {} by A8;
hence P₁[y1 ^ x2] by A1, A7, A9; :: thesis: verum

end;

A10: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A11: for x1, x2, y1, y2 being FinSequence st len x1 = i & F₁() = x1 ^ x2 & len y1 = i & F₂() = y1 ^ y2 holds
P₁[y1 ^ x2] ; :: thesis: S₁[i + 1]
let x1, x2, y1, y2 be FinSequence; :: thesis: ( len x1 = i + 1 & F₁() = x1 ^ x2 & len y1 = i + 1 & F₂() = y1 ^ y2 implies P₁[y1 ^ x2] )
assume that
A12: len x1 = i + 1 and
A13: F₁() = x1 ^ x2 and
A14: len y1 = i + 1 and
A15: F₂() = y1 ^ y2 ; :: thesis: P₁[y1 ^ x2]
A16: x1 <> {} by A12;
A17: y1 <> {} by A14;
consider x9 being FinSequence, xx being object such that
A18: x1 = x9 ^ <*xx*> by A16, FINSEQ_1:46;
consider y9 being FinSequence, yy being object such that
A19: y1 = y9 ^ <*yy*> by A17, FINSEQ_1:46;
A20: dom x1 = Seg (len x1) by FINSEQ_1:def 3;
A21: dom y1 = Seg (len y1) by FINSEQ_1:def 3;
A22: len <*xx*> = 1 by FINSEQ_1:40;
A23: len <*yy*> = 1 by FINSEQ_1:40;
A24: len x1 = (len x9) + 1 by A18, A22, FINSEQ_1:22;
A25: len y1 = (len y9) + 1 by A19, A23, FINSEQ_1:22;
A26: F₁() = x9 ^ (<*xx*> ^ x2) by A13, A18, FINSEQ_1:32;
A27: F₂() = y9 ^ (<*yy*> ^ y2) by A15, A19, FINSEQ_1:32;
A28: i + 1 in dom x1 by A12, A20, FINSEQ_1:4;
A29: dom x1 c= dom F₁() by A13, FINSEQ_1:26;
A30: x1 . ((len x9) + 1) = xx by A18, FINSEQ_1:42;
A31: y1 . ((len y9) + 1) = yy by A19, FINSEQ_1:42;
A32: P₁[y9 ^ (<*xx*> ^ x2)] by A11, A12, A14, A24, A25, A26, A27;
A33: F₁() . (i + 1) = xx by A12, A13, A24, A28, A30, FINSEQ_1:def 7;
A34: F₂() . (i + 1) = yy by A12, A14, A15, A20, A21, A25, A28, A31, FINSEQ_1:def 7;
P₁[(y9 ^ <*xx*>) ^ x2] by A32, FINSEQ_1:32;
hence P₁[y1 ^ x2] by A3, A4, A19, A28, A29, A33, A34; :: thesis: verum

end;

A35: for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A10);
A36: F₁() = F₁() ^ {} by FINSEQ_1:34;
F₂() = F₂() ^ {} by FINSEQ_1:34;
hence P₁[F₂()] by A2, A35, A36; :: thesis: verum