let f be FinSequence; :: thesis: for g being FinSequence holds Rev (f ^ g) = (Rev g) ^ (Rev f)
defpred S₁[ FinSequence] means Rev (f ^ $1) = (Rev $1) ^ (Rev f);
A1: S₁[ {} ]

proof

set g = {} ;
thus Rev (f ^ {}) = Rev f by FINSEQ_1:34
.= (Rev {}) ^ (Rev f) by FINSEQ_1:34 ; :: thesis: verum

end;

A2: for g being FinSequence
for x being object st S₁[g] holds
S₁[g ^ <*x*>]

proof

let g be FinSequence; :: thesis: for x being object st S₁[g] holds
S₁[g ^ <*x*>]
let x be object ; :: thesis: ( S₁[g] implies S₁[g ^ <*x*>] )
assume A3: S₁[g] ; :: thesis: S₁[g ^ <*x*>]
thus Rev (f ^ (g ^ <*x*>)) = Rev ((f ^ g) ^ <*x*>) by FINSEQ_1:32
.= <*x*> ^ ((Rev g) ^ (Rev f)) by A3, Th63
.= (<*x*> ^ (Rev g)) ^ (Rev f) by FINSEQ_1:32
.= (Rev (g ^ <*x*>)) ^ (Rev f) by Th63 ; :: thesis: verum

end;

thus for g being FinSequence holds S₁[g] from FINSEQ_1:sch 3(A1, A2); :: thesis: verum