let x, y be set ; :: thesis: for f, g being FinSequence st <*x*> ^ f = <*y*> ^ g holds
f = g
let f, g be FinSequence; :: thesis: ( <*x*> ^ f = <*y*> ^ g implies f = g )
assume A1: <*x*> ^ f = <*y*> ^ g ; :: thesis: f = g
then x = (<*y*> ^ g) . 1 by FINSEQ_1:41
.= y by FINSEQ_1:41 ;
hence f = g by A1, FINSEQ_1:33; :: thesis: verum