defpred S₁[ Element of 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 A6: ( len x1 = 0 & F₁() = x1 ^ x2 & len y1 = 0 & F₂() = y1 ^ y2 ) ; :: thesis: P₁[y1 ^ x2]
then ( x1 = {} & y1 = {} ) ;
hence P₁[y1 ^ x2] by A1, A6; :: thesis: verum

end;

A7: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A8: 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 A9: ( len x1 = i + 1 & F₁() = x1 ^ x2 & len y1 = i + 1 & F₂() = y1 ^ y2 ) ; :: thesis: P₁[y1 ^ x2]
A10: ( x1 <> {} & y1 <> {} ) by A9;
then consider x' being FinSequence, xx being set such that
A11: x1 = x' ^ <*xx*> by FINSEQ_1:63;
consider y' being FinSequence, yy being set such that
A12: y1 = y' ^ <*yy*> by A10, FINSEQ_1:63;
A13: ( dom x1 = Seg (len x1) & dom y1 = Seg (len y1) ) by FINSEQ_1:def 3;
( len <*xx*> = 1 & len <*yy*> = 1 ) by FINSEQ_1:57;
then ( len x1 = (len x') + 1 & len y1 = (len y') + 1 ) by A11, A12, FINSEQ_1:35;
then ( len x' = i & F₁() = x' ^ (<*xx*> ^ x2) & len y' = i & F₂() = y' ^ (<*yy*> ^ y2) & i + 1 in dom x1 & dom x1 c= dom F₁() & x1 . ((len x') + 1) = xx & y1 . ((len y') + 1) = yy ) by A9, A11, A12, A13, FINSEQ_1:6, FINSEQ_1:39, FINSEQ_1:45, FINSEQ_1:59;
then ( P₁[y' ^ (<*xx*> ^ x2)] & i + 1 in dom F₁() & F₁() . (i + 1) = xx & F₂() . (i + 1) = yy ) by A8, A9, A13, FINSEQ_1:def 7;
then ( P₁[(y' ^ <*xx*>) ^ x2] & P₂[xx,yy] ) by A4, FINSEQ_1:45;
hence P₁[y1 ^ x2] by A3, A12; :: thesis: verum

end;

A14: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A5, A7);
( F₁() = F₁() ^ {} & F₂() = F₂() ^ {} ) by FINSEQ_1:47;
hence P₁[F₂()] by A2, A14; :: thesis: verum