let I, J be FinSequence-membered set ; :: thesis: for f being FinSequence holds
( I c= J iff f ^^ I c= f ^^ J )
let f be FinSequence; :: thesis: ( I c= J iff f ^^ I c= f ^^ J )
thus ( I c= J implies f ^^ I c= f ^^ J ) :: thesis: ( f ^^ I c= f ^^ J implies I c= J )
proof
assume A1: I c= J ; :: thesis: f ^^ I c= f ^^ J
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f ^^ I or a in f ^^ J )
assume a in f ^^ I ; :: thesis: a in f ^^ J
then ex b being Element of I st
( a = f ^ b & b in I ) ;
hence a in f ^^ J by A1; :: thesis: verum
end;
assume A2: f ^^ I c= f ^^ J ; :: thesis: I c= J
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in I or a in J )
assume A3: a in I ; :: thesis: a in J
then reconsider a = a as FinSequence ;
f ^ a in f ^^ I by A3;
then f ^ a in f ^^ J by A2;
then consider b being Element of J such that
A4: ( f ^ a = f ^ b & b in J ) ;
thus a in J by A4, FINSEQ_1:33; :: thesis: verum